![]() |
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 1116 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp31 1109 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: 3comr 1122 3coml 1124 oacan 8570 oaword1 8574 nnacan 8650 nnaword1 8651 elmapg 8860 fisseneq 9284 ltapr 11079 subadd 11504 ltaddsub 11729 leaddsub 11731 iooshf 13451 faclbnd4 14309 relexpsucl 15031 relexpsucr 15032 dvdsmulc 16281 lcmdvdsb 16609 infpnlem1 16907 fmf 23937 frgr3v 30205 nvs 30593 dipdi 30773 dipsubdi 30779 spansncol 31498 chirredlem2 32321 mdsymlem3 32335 isbasisrelowllem2 37076 ltflcei 37322 iscringd 37712 resubadd 42090 iunrelexp0 43406 uun123p4 44525 isosctrlem1ALT 44647 stoweidlem17 45674 |
Copyright terms: Public domain | W3C validator |