Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > com13 | Unicode version |
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.) |
Ref | Expression |
---|---|
com3.1 |
Ref | Expression |
---|---|
com13 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com3.1 | . . 3 | |
2 | 1 | com3r 79 | . 2 |
3 | 2 | com23 78 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com24 87 an13s 557 an31s 560 3imp31 1185 3imp21 1187 funopg 5216 f1o2ndf1 6187 brecop 6582 fiintim 6885 elpq 9577 xnn0lenn0nn0 9792 elfz0ubfz0 10050 elfz0fzfz0 10051 fz0fzelfz0 10052 fz0fzdiffz0 10055 fzo1fzo0n0 10108 elfzodifsumelfzo 10126 ssfzo12 10149 ssfzo12bi 10150 facwordi 10642 fihashf1rn 10691 oddnn02np1 11802 oddge22np1 11803 evennn02n 11804 evennn2n 11805 dfgcd2 11932 sqrt2irr 12073 bj-inf2vnlem2 13694 |
Copyright terms: Public domain | W3C validator |