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

Theorem 3imtr3i 290
Description: A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)
Hypotheses
Ref Expression
3imtr3.1 (𝜑𝜓)
3imtr3.2 (𝜑𝜒)
3imtr3.3 (𝜓𝜃)
Assertion
Ref Expression
3imtr3i (𝜒𝜃)

Proof of Theorem 3imtr3i
StepHypRef Expression
1 3imtr3.2 . . 3 (𝜑𝜒)
2 3imtr3.1 . . 3 (𝜑𝜓)
31, 2sylbir 234 . 2 (𝜒𝜓)
4 3imtr3.3 . 2 (𝜓𝜃)
53, 4sylib 217 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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
This theorem is referenced by:  rb-ax1  1754  speimfwALT  1968  cbv1v  2332  cbv1  2400  hblem  2869  hblemg  2870  nfcriiOLD  2899  sbhypf  3506  axrep1  5242  tfinds2  7797  smores  8295  idssen  8934  1sdomOLD  9190  ssttrcl  9648  itunitc1  10353  dominf  10378  dominfac  10506  ssxr  11221  nnwos  12837  pmatcollpw3lem  22128  ppttop  22353  ptclsg  22962  sincosq3sgn  25853  adjbdln  30923  fmptdF  31470  funcnv4mpt  31483  disjdsct  31512  esumpcvgval  32568  esumcvg  32576  measiuns  32707  ballotlemodife  32988  bnj605  33410  bnj594  33415  acycgr0v  33633  prclisacycgr  33636  imagesset  34527  meran1  34872  meran3  34874  bj-modal4e  35169  f1omptsnlem  35796  mptsnunlem  35798  topdifinffinlem  35807  relowlpssretop  35824  poimirlem25  36092  eqbrb  36679  eqelb  36681  symrefref3  37015  dedths  37413  sn-axrep5v  40626  dffltz  40948  mzpincl  41033  lerabdioph  41104  ltrabdioph  41107  nerabdioph  41108  dvdsrabdioph  41109  finona1cl  41705  frege91  42206  frege97  42212  frege98  42213  frege109  42224  sumnnodd  43841  aiotaval  45297  rrx2linest  46798
  Copyright terms: Public domain W3C validator