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 1127 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 3imp3i2an.3 | . 2 ⊢ ((𝜃 ∧ 𝜏) → 𝜂) | |
5 | 1, 3, 4 | syl2anc 586 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: ordunel 7544 distrlem5pr 10451 divmul 11303 modmulnn 13260 moddi 13310 repswpfx 14149 shftval2 14436 pcgcd 16216 gsumccatOLD 18007 gsumccat 18008 qussub 18342 gsumdixp 19361 lspun 19761 evlslem4 20290 scmatrngiso 21147 ordtcld3 21809 fusgrfisstep 27113 cplgr3v 27219 upgr2pthnlp 27515 frgrreg 28175 eliuniin 41372 eliuniin2 41393 |
Copyright terms: Public domain | W3C validator |