![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3imp3i2an | Structured version Visualization version GIF version |
Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.) |
Ref | Expression |
---|---|
3imp3i2an.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
3imp3i2an.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
3imp3i2an.3 | ⊢ ((𝜃 ∧ 𝜏) → 𝜂) |
Ref | Expression |
---|---|
3imp3i2an | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imp3i2an.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 3imp3i2an.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜏) | |
3 | 2 | 3adant2 1122 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 3imp3i2an.3 | . 2 ⊢ ((𝜃 ∧ 𝜏) → 𝜂) | |
5 | 1, 3, 4 | syl2anc 579 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 1073 |
This theorem is referenced by: ordunel 7307 distrlem5pr 10186 divmul 11039 modmulnn 13012 moddi 13062 shftval2 14228 pcgcd 15997 gsumccat 17775 qussub 18049 gsumdixp 19007 lspun 19393 evlslem4 19915 scmatrngiso 20758 ordtcld3 21422 cplgr3v 26800 upgr2pthnlp 27101 frgrreg 27843 eliuniin 40224 eliuniin2 40246 |
Copyright terms: Public domain | W3C validator |