![]() |
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 1132 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 3imp3i2an.3 | . 2 ⊢ ((𝜃 ∧ 𝜏) → 𝜂) | |
5 | 1, 3, 4 | syl2anc 585 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: focofo 6819 ordunel 7815 naddel1 8686 distrlem5pr 11022 divmul 11875 modmulnn 13854 moddi 13904 repswpfx 14735 shftval2 15022 pcgcd 16811 gsumccat 18722 qussub 19070 gsumdixp 20131 lspun 20598 evlslem4 21637 ordtcld3 22703 sleadd1im 27470 fusgrfisstep 28586 cplgr3v 28692 upgr2pthnlp 28989 frgrreg 29647 eliuniin 43788 eliuniin2 43809 disjinfi 43891 |
Copyright terms: Public domain | W3C validator |