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

Theorem 3imtr3i 265
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 213 . 2
4 3imtr3.3 . 2
53, 4sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  rb-ax1  1585  speimfwOLD  1736  cbv1  2017  hblem  2580  axrep1  4564  tfinds2  6698  smores  7042  idssen  7580  1sdom  7742  itunitc1  8821  dominf  8846  dominfac  8969  ssxr  9675  ltadd2iOLD  9737  nnwos  11178  pmatcollpw3lem  19284  ppttop  19508  ptclsg  20116  sincosq3sgn  22893  adjbdln  27002  fmptdF  27495  funcnv4mpt  27512  disjdsct  27521  esumpcvgval  28084  esumcvg  28092  measiuns  28188  ballotlemodife  28436  imagesset  29603  meran1  29876  meran3  29878  mzpincl  30666  lerabdioph  30738  ltrabdioph  30741  nerabdioph  30742  dvdsrabdioph  30743  sumnnodd  31636  bnj605  33965  bnj594  33970  bj-nalnaleximiOLD  34222  bj-cbv1v  34292  bj-axrep1  34374  bj-hblem  34425  dedths  34693
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 185
  Copyright terms: Public domain W3C validator