![]() |
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 8548 oaword1 8552 nnacan 8628 nnaword1 8629 elmapg 8833 fisseneq 9257 ltapr 11040 subadd 11463 ltaddsub 11688 leaddsub 11690 iooshf 13403 faclbnd4 14257 relexpsucl 14978 relexpsucr 14979 dvdsmulc 16227 lcmdvdsb 16550 infpnlem1 16843 fmf 23449 frgr3v 29559 nvs 29947 dipdi 30127 dipsubdi 30133 spansncol 30852 chirredlem2 31675 mdsymlem3 31689 isbasisrelowllem2 36285 ltflcei 36524 iscringd 36914 resubadd 41300 iunrelexp0 42501 uun123p4 43621 isosctrlem1ALT 43743 stoweidlem17 44781 |
Copyright terms: Public domain | W3C validator |