![]() |
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 1130 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
4 | 3imp3i2an.3 | . 2 ⊢ ((𝜃 ∧ 𝜏) → 𝜂) | |
5 | 1, 3, 4 | syl2anc 584 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: focofo 6834 ordunel 7847 naddel1 8724 distrlem5pr 11065 divmul 11923 modmulnn 13926 moddi 13977 repswpfx 14820 shftval2 15111 pcgcd 16912 gsumccat 18867 qussub 19222 gsumdixp 20333 lspun 21003 evlslem4 22118 ordtcld3 23223 sleadd1im 28035 fusgrfisstep 29361 cplgr3v 29467 upgr2pthnlp 29765 frgrreg 30423 eliuniin 45039 eliuniin2 45060 disjinfi 45135 |
Copyright terms: Public domain | W3C validator |