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 583 1 ((𝜑𝜓𝜒) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 396  df-3an 1087
This theorem is referenced by:  focofo  6818  ordunel  7822  naddel1  8699  distrlem5pr  11036  divmul  11891  modmulnn  13872  moddi  13922  repswpfx  14753  shftval2  15040  pcgcd  16832  gsumccat  18778  qussub  19130  gsumdixp  20237  lspun  20853  evlslem4  21998  ordtcld3  23077  sleadd1im  27878  fusgrfisstep  29116  cplgr3v  29222  upgr2pthnlp  29520  frgrreg  30178  eliuniin  44378  eliuniin2  44399  disjinfi  44478
  Copyright terms: Public domain W3C validator