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 557 an31s 560 3imp31 1185 3imp21 1187 funopg 5219 f1o2ndf1 6190 brecop 6585 fiintim 6888 elpq 9580 xnn0lenn0nn0 9795 elfz0ubfz0 10054 elfz0fzfz0 10055 fz0fzelfz0 10056 fz0fzdiffz0 10059 fzo1fzo0n0 10112 elfzodifsumelfzo 10130 ssfzo12 10153 ssfzo12bi 10154 facwordi 10647 fihashf1rn 10696 oddnn02np1 11811 oddge22np1 11812 evennn02n 11813 evennn2n 11814 dfgcd2 11941 sqrt2irr 12088 bj-inf2vnlem2 13746 |
Copyright terms: Public domain | W3C validator |