![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > com13 | GIF 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 567 an31s 570 3imp31 1196 3imp21 1198 funopg 5250 f1o2ndf1 6228 brecop 6624 fiintim 6927 elpq 9647 xnn0lenn0nn0 9864 elfz0ubfz0 10124 elfz0fzfz0 10125 fz0fzelfz0 10126 fz0fzdiffz0 10129 fzo1fzo0n0 10182 elfzodifsumelfzo 10200 ssfzo12 10223 ssfzo12bi 10224 facwordi 10719 fihashf1rn 10767 oddnn02np1 11884 oddge22np1 11885 evennn02n 11886 evennn2n 11887 dfgcd2 12014 sqrt2irr 12161 zabsle1 14370 bj-inf2vnlem2 14693 |
Copyright terms: Public domain | W3C validator |