Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > an32s | Unicode version |
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.) |
Ref | Expression |
---|---|
an32s.1 |
Ref | Expression |
---|---|
an32s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an32 526 | . 2 | |
2 | an32s.1 | . 2 | |
3 | 1, 2 | sylbi 119 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: anass1rs 535 anabss1 540 fssres 5086 foco 5136 fun11iun 5167 fconstfvm 5400 isocnv 5471 f1oiso 5485 f1ocnvfv3 5521 findcard 6372 genpassl 6714 genpassu 6715 cnegexlem3 7285 recexaplem2 7742 divap0 7772 dfinfre 8034 qreccl 8727 xrlttr 8870 addmodlteq 9400 cau3lem 10000 climcn1 10147 climcn2 10148 climcaucn 10188 rplpwr 10416 dvdssq 10420 nn0seqcvgd 10423 lcmgcdlem 10459 isprm6 10526 |
Copyright terms: Public domain | W3C validator |