![]() |
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 1145 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | 3imp 1140 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 927 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: 3coml 1153 syld3an2 1228 3anidm13 1239 eqreu 2821 f1ofveu 5678 acexmid 5689 dfsmo2 6090 f1oeng 6554 ltexprlemdisj 7262 ltexprlemfu 7267 recexprlemss1u 7292 mul32 7709 add32 7738 cnegexlem2 7755 subsub23 7784 subadd23 7791 addsub12 7792 subsub 7809 subsub3 7811 sub32 7813 suble 8015 lesub 8016 ltsub23 8017 ltsub13 8018 ltleadd 8021 div32ap 8256 div13ap 8257 div12ap 8258 divdiv32ap 8284 cju 8519 icc0r 9492 fzen 9606 elfz1b 9653 ioo0 9820 ico0 9822 ioc0 9823 expgt0 10103 expge0 10106 expge1 10107 shftval2 10375 abs3dif 10653 divalgb 11352 restin 12028 cnpnei 12070 cnptoprest 12090 psmetsym 12115 xmetsym 12154 |
Copyright terms: Public domain | W3C validator |