Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3com13 | Structured version Visualization version GIF version |
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3com13 | ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1121 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp31 1114 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1091 |
This theorem is referenced by: 3comr 1127 3coml 1129 oacan 8273 oaword1 8277 nnacan 8353 nnaword1 8354 elmapg 8518 fisseneq 8886 ltapr 10656 subadd 11078 ltaddsub 11303 leaddsub 11305 iooshf 13011 faclbnd4 13860 relexpsucl 14591 relexpsucr 14592 dvdsmulc 15842 lcmdvdsb 16167 infpnlem1 16460 fmf 22839 frgr3v 28355 nvs 28741 dipdi 28921 dipsubdi 28927 spansncol 29646 chirredlem2 30469 mdsymlem3 30483 isbasisrelowllem2 35261 ltflcei 35500 iscringd 35891 resubadd 40068 iunrelexp0 40985 uun123p4 42103 isosctrlem1ALT 42225 stoweidlem17 43231 |
Copyright terms: Public domain | W3C validator |