![]() |
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 1152 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp31 1143 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1111 |
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 199 df-an 387 df-3an 1113 |
This theorem is referenced by: 3comr 1159 3coml 1161 3adant3lOLD 1234 3adant3rOLD 1236 syld3an1OLD 1534 oacan 7895 oaword1 7899 nnacan 7975 nnaword1 7976 elmapg 8135 fisseneq 8440 ltapr 10182 subadd 10604 ltaddsub 10826 leaddsub 10828 iooshf 12540 faclbnd4 13377 relexpsucr 14146 relexpsucl 14150 dvdsmulc 15386 lcmdvdsb 15699 infpnlem1 15985 fmf 22119 frgr3v 27645 nvs 28062 dipdi 28242 dipsubdi 28248 spansncol 28971 chirredlem2 29794 mdsymlem3 29808 isbasisrelowllem2 33742 ltflcei 33933 iscringd 34332 resubadd 38077 iunrelexp0 38828 uun123p4 39859 isosctrlem1ALT 39981 stoweidlem17 41021 |
Copyright terms: Public domain | W3C validator |