![]() |
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 1202 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | 3imp 1193 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3coml 1210 syld3an2 1285 3anidm13 1296 eqreu 2931 f1ofveu 5865 acexmid 5876 dfsmo2 6290 f1oeng 6759 ctssdc 7114 ltexprlemdisj 7607 ltexprlemfu 7612 recexprlemss1u 7637 mul32 8089 add32 8118 cnegexlem2 8135 subsub23 8164 subadd23 8171 addsub12 8172 subsub 8189 subsub3 8191 sub32 8193 suble 8399 lesub 8400 ltsub23 8401 ltsub13 8402 ltleadd 8405 div32ap 8651 div13ap 8652 div12ap 8653 divdiv32ap 8679 cju 8920 icc0r 9928 fzen 10045 elfz1b 10092 ioo0 10262 ico0 10264 ioc0 10265 expgt0 10555 expge0 10558 expge1 10559 shftval2 10837 abs3dif 11116 divalgb 11932 nnwodc 12039 ctinf 12433 grpinvcnv 12943 mulgaddcom 13012 mulgneg2 13022 srgrmhm 13182 ringcom 13219 mulgass2 13240 opprring 13254 unitmulcl 13287 islmodd 13388 lmodcom 13428 rmodislmod 13446 restin 13761 cnpnei 13804 cnptoprest 13824 psmetsym 13914 xmetsym 13953 |
Copyright terms: Public domain | W3C validator |