Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3com23 | GIF version |
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3com23 | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1184 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | 3imp 1176 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 3coml 1192 syld3an2 1267 3anidm13 1278 eqreu 2904 f1ofveu 5812 acexmid 5823 dfsmo2 6234 f1oeng 6702 ctssdc 7057 ltexprlemdisj 7526 ltexprlemfu 7531 recexprlemss1u 7556 mul32 8005 add32 8034 cnegexlem2 8051 subsub23 8080 subadd23 8087 addsub12 8088 subsub 8105 subsub3 8107 sub32 8109 suble 8315 lesub 8316 ltsub23 8317 ltsub13 8318 ltleadd 8321 div32ap 8565 div13ap 8566 div12ap 8567 divdiv32ap 8593 cju 8832 icc0r 9830 fzen 9945 elfz1b 9992 ioo0 10159 ico0 10161 ioc0 10162 expgt0 10452 expge0 10455 expge1 10456 shftval2 10726 abs3dif 11005 divalgb 11816 ctinf 12170 restin 12587 cnpnei 12630 cnptoprest 12650 psmetsym 12740 xmetsym 12779 |
Copyright terms: Public domain | W3C validator |