| 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 584 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: focofo 6833 ordunel 7847 naddel1 8725 distrlem5pr 11067 divmul 11925 modmulnn 13929 moddi 13980 repswpfx 14823 shftval2 15114 pcgcd 16916 gsumccat 18854 qussub 19209 gsumdixp 20316 lspun 20985 evlslem4 22100 ordtcld3 23207 sleadd1im 28020 fusgrfisstep 29346 cplgr3v 29452 upgr2pthnlp 29752 frgrreg 30413 eliuniin 45104 eliuniin2 45125 disjinfi 45197 |
| Copyright terms: Public domain | W3C validator |