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

Theorem 3imp3i2an 1346
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 1132 . 2 ((𝜑𝜓𝜒) → 𝜏)
4 3imp3i2an.3 . 2 ((𝜃𝜏) → 𝜂)
51, 3, 4syl2anc 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