MPE Home 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