additional df-ich theorems (metamath#3654)

+ ichv
+ ichf
+ ich2al
+ ich2ex

set.mm

@@ -726003,6 +726003,26 @@ valid cases ( ` (/) ` is the last symbol) and invalid cases ( ` (/) `
       $.
   $}
 
+  ${
+    $d a x ph $.  $d a y ph $.
+    $( Setvar variables are interchangeable in a wff they do not appear in.
+       (Contributed by SN, 23-Nov-2023.) $)
+    ichv $p |- [ x <> y ] ph $=
+      ( va wich wsb wb wal sbv sbbii bitri gen2 df-ich mpbir ) ABCEACDFZBCFZDBF
+      ZAGZCHBHRBCQADBFAPADBPABCFAOABCACDIJABCIKJADBIKLABCDMN $.
+  $}
+
+  ${
+    $d a x $.  $d a y $.  $d a ph $.
+    ichf.1 $e |- F/ x ph $.
+    ichf.2 $e |- F/ y ph $.
+    $( Setvar variables are interchangeable in a wff they are not free in.
+       (Contributed by SN, 23-Nov-2023.) $)
+    ichf $p |- [ x <> y ] ph $=
+      ( va wich wsb wb wal sbf sbbii bitri sbv gen2 df-ich mpbir ) ABCGACFHZBCH
+      ZFBHZAIZCJBJUABCTAFBHASAFBSABCHARABCACFEKLABCDKMLAFBNMOABCFPQ $.
+  $}
+
   ${
     $d a ph $.  $d a x $.
     $( A setvar variable is always interchangeable with itself.  (Contributed
@@ -726188,6 +726208,16 @@ valid cases ( ` (/) ` is the last symbol) and invalid cases ( ` (/) `
       DETUAUJCDETUB $.
   $}
 
+  $( Two setvar variables are always interchangeable when there are two
+     universal quantifiers.  (Contributed by SN, 23-Nov-2023.) $)
+  ich2al $p |- [ x <> y ] A. x A. y ph $=
+    ( wal nfa1 nfa2 ichf ) ACDZBDBCHBEACBFG $.
+
+  $( Two setvar variables are always interchangeable when there are two
+     existential quantifiers.  (Contributed by SN, 23-Nov-2023.) $)
+  ich2ex $p |- [ x <> y ] E. x E. y ph $=
+    ( wex nfe1 excom nfxfr ichf ) ACDZBDZBCIBEJABDZCDCABCFKCEGH $.
+
   ${
     $d ph x y $.  $d ps x y $.  $d a b x y $.
     $( If two setvar variables are interchangeable in two wffs, then they are