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 73 | . 2 |
3 | 2 | com23 72 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com24 81 an13s 501 an31s 504 funopg 4934 f1o2ndf1 5849 brecop 6196 elfz0ubfz0 8982 elfz0fzfz0 8983 fz0fzelfz0 8984 fz0fzdiffz0 8987 fzo1fzo0n0 9039 elfzodifsumelfzo 9057 ssfzo12 9080 ssfzo12bi 9081 sqrt2irr 9878 bj-inf2vnlem2 10096 |
Copyright terms: Public domain | W3C validator |