![]() |
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 1119 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp31 1112 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: 3comr 1125 3coml 1127 oacan 8487 oaword1 8491 nnacan 8567 nnaword1 8568 elmapg 8736 fisseneq 9159 ltapr 10939 subadd 11362 ltaddsub 11587 leaddsub 11589 iooshf 13297 faclbnd4 14151 relexpsucl 14876 relexpsucr 14877 dvdsmulc 16126 lcmdvdsb 16449 infpnlem1 16742 fmf 23248 frgr3v 29048 nvs 29434 dipdi 29614 dipsubdi 29620 spansncol 30339 chirredlem2 31162 mdsymlem3 31176 isbasisrelowllem2 35765 ltflcei 36004 iscringd 36395 resubadd 40757 iunrelexp0 41885 uun123p4 43005 isosctrlem1ALT 43127 stoweidlem17 44159 |
Copyright terms: Public domain | W3C validator |