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 1111 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp31 1104 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3comr 1117 3coml 1119 oacan 8163 oaword1 8167 nnacan 8243 nnaword1 8244 elmapg 8408 fisseneq 8717 ltapr 10455 subadd 10877 ltaddsub 11102 leaddsub 11104 iooshf 12803 faclbnd4 13645 relexpsucr 14376 relexpsucl 14380 dvdsmulc 15625 lcmdvdsb 15945 infpnlem1 16234 fmf 22481 frgr3v 27981 nvs 28367 dipdi 28547 dipsubdi 28553 spansncol 29272 chirredlem2 30095 mdsymlem3 30109 isbasisrelowllem2 34519 ltflcei 34761 iscringd 35157 resubadd 39087 iunrelexp0 39925 uun123p4 41023 isosctrlem1ALT 41145 stoweidlem17 42179 |
Copyright terms: Public domain | W3C validator |