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 556 an31s 559 funopg 5157 f1o2ndf1 6125 brecop 6519 fiintim 6817 xnn0lenn0nn0 9648 elfz0ubfz0 9902 elfz0fzfz0 9903 fz0fzelfz0 9904 fz0fzdiffz0 9907 fzo1fzo0n0 9960 elfzodifsumelfzo 9978 ssfzo12 10001 ssfzo12bi 10002 facwordi 10486 fihashf1rn 10535 oddnn02np1 11577 oddge22np1 11578 evennn02n 11579 evennn2n 11580 dfgcd2 11702 sqrt2irr 11840 bj-inf2vnlem2 13169 |
Copyright terms: Public domain | W3C validator |