![]() |
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: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com24 87 an13s 567 an31s 570 3imp31 1196 3imp21 1198 funopg 5246 f1o2ndf1 6223 brecop 6619 fiintim 6922 elpq 9637 xnn0lenn0nn0 9852 elfz0ubfz0 10111 elfz0fzfz0 10112 fz0fzelfz0 10113 fz0fzdiffz0 10116 fzo1fzo0n0 10169 elfzodifsumelfzo 10187 ssfzo12 10210 ssfzo12bi 10211 facwordi 10704 fihashf1rn 10752 oddnn02np1 11868 oddge22np1 11869 evennn02n 11870 evennn2n 11871 dfgcd2 11998 sqrt2irr 12145 zabsle1 14067 bj-inf2vnlem2 14379 |
Copyright terms: Public domain | W3C validator |