![]() |
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 1120 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp31 1113 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: 3comr 1126 3coml 1128 oacan 8499 oaword1 8503 nnacan 8579 nnaword1 8580 elmapg 8784 fisseneq 9207 ltapr 10989 subadd 11412 ltaddsub 11637 leaddsub 11639 iooshf 13352 faclbnd4 14206 relexpsucl 14925 relexpsucr 14926 dvdsmulc 16174 lcmdvdsb 16497 infpnlem1 16790 fmf 23319 frgr3v 29268 nvs 29654 dipdi 29834 dipsubdi 29840 spansncol 30559 chirredlem2 31382 mdsymlem3 31396 isbasisrelowllem2 35877 ltflcei 36116 iscringd 36507 resubadd 40895 iunrelexp0 42066 uun123p4 43186 isosctrlem1ALT 43308 stoweidlem17 44348 |
Copyright terms: Public domain | W3C validator |