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 7536 distrlem5pr 10443 divmul 11295 modmulnn 13251 moddi 13301 repswpfx 14141 shftval2 14428 pcgcd 16208 gsumccatOLD 17999 gsumccat 18000 qussub 18334 gsumdixp 19353 lspun 19753 evlslem4 20282 scmatrngiso 21139 ordtcld3 21801 fusgrfisstep 27105 cplgr3v 27211 upgr2pthnlp 27507 frgrreg 28167 eliuniin 41358 eliuniin2 41379 |
Copyright terms: Public domain | W3C validator |