Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imp3i2an Structured version   Visualization version   GIF version

Theorem 3imp3i2an 1341
 Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)
Hypotheses
Ref Expression
3imp3i2an.1 ((𝜑𝜓𝜒) → 𝜃)
3imp3i2an.2 ((𝜑𝜒) → 𝜏)
3imp3i2an.3 ((𝜃𝜏) → 𝜂)
Assertion
Ref Expression
3imp3i2an ((𝜑𝜓𝜒) → 𝜂)

Proof of Theorem 3imp3i2an
StepHypRef Expression
1 3imp3i2an.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
2 3imp3i2an.2 . . 3 ((𝜑𝜒) → 𝜏)
323adant2 1127 . 2 ((𝜑𝜓𝜒) → 𝜏)
4 3imp3i2an.3 . 2 ((𝜃𝜏) → 𝜂)
51, 3, 4syl2anc 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  7541  distrlem5pr  10448  divmul  11300  modmulnn  13256  moddi  13306  repswpfx  14146  shftval2  14433  pcgcd  16213  gsumccatOLD  18004  gsumccat  18005  qussub  18339  gsumdixp  19358  lspun  19758  evlslem4  20287  scmatrngiso  21144  ordtcld3  21806  fusgrfisstep  27110  cplgr3v  27216  upgr2pthnlp  27512  frgrreg  28172  eliuniin  41365  eliuniin2  41386
 Copyright terms: Public domain W3C validator