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

Theorem 3imp3i2an 1343
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 1129 . 2 ((𝜑𝜓𝜒) → 𝜏)
4 3imp3i2an.3 . 2 ((𝜃𝜏) → 𝜂)
51, 3, 4syl2anc 582 1 ((𝜑𝜓𝜒) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085
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 206  df-an 395  df-3an 1087
This theorem is referenced by:  focofo  6817  ordunel  7817  naddel1  8688  distrlem5pr  11024  divmul  11879  modmulnn  13858  moddi  13908  repswpfx  14739  shftval2  15026  pcgcd  16815  gsumccat  18758  qussub  19106  gsumdixp  20207  lspun  20742  evlslem4  21856  ordtcld3  22923  sleadd1im  27709  fusgrfisstep  28853  cplgr3v  28959  upgr2pthnlp  29256  frgrreg  29914  eliuniin  44089  eliuniin2  44110  disjinfi  44189
  Copyright terms: Public domain W3C validator