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

Theorem 3imtr3i 280
 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 225 . 2 (𝜒𝜓)
4 3imtr3.3 . 2 (𝜓𝜃)
53, 4sylib 208 1 (𝜒𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  rb-ax1  1717  speimfwALT  1934  cbv1  2303  hblem  2760  axrep1  4805  tfinds2  7105  smores  7494  idssen  8042  1sdom  8204  itunitc1  9280  dominf  9305  dominfac  9433  ssxr  10145  nnwos  11793  pmatcollpw3lem  20636  ppttop  20859  ptclsg  21466  sincosq3sgn  24297  adjbdln  29070  fmptdF  29584  funcnv4mpt  29598  disjdsct  29608  esumpcvgval  30268  esumcvg  30276  measiuns  30408  ballotlemodife  30687  bnj605  31103  bnj594  31108  imagesset  32185  meran1  32535  meran3  32537  bj-modal4e  32830  bj-cbv1v  32854  bj-axrep1  32913  bj-hblem  32974  f1omptsnlem  33313  mptsnunlem  33315  topdifinffinlem  33325  relowlpssretop  33342  poimirlem25  33564  eqelb  34145  symrefref3  34448  dedths  34566  mzpincl  37614  lerabdioph  37686  ltrabdioph  37689  nerabdioph  37690  dvdsrabdioph  37691  frege91  38565  frege97  38571  frege98  38572  frege109  38583  sumnnodd  40180
 Copyright terms: Public domain W3C validator