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

Theorem 3imtr4i 274
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3imtr4.1  |-  ( ph  ->  ps )
3imtr4.2  |-  ( ch  <->  ph )
3imtr4.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3imtr4i  |-  ( ch 
->  th )

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3  |-  ( ch  <->  ph )
2 3imtr4.1 . . 3  |-  ( ph  ->  ps )
31, 2sylbi 200 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 217 1  |-  ( ch 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  hbxfrbi  1702  sbimi  1811  ralimi2  2793  reximi2  2851  r19.28v  2911  r19.29r  2913  r19.30  2921  elex  3040  rmoan  3226  rmoimi2  3229  sseq2  3440  rabss2  3498  undif4  3825  r19.2zb  3850  ralf0  3867  difprsnss  4098  snsspw  4135  uniin  4210  iuniin  4280  iuneq1  4283  iuneq2  4286  iunpwss  4364  eunex  4594  rmorabex  4660  exss  4663  pwunss  4744  soeq2  4780  elopaelxp  4912  reliin  4960  coeq1  4997  coeq2  4998  cnveq  5013  dmeq  5040  dmin  5048  dmcoss  5100  rncoeq  5104  dminss  5256  imainss  5257  dfco2a  5342  iotaex  5570  fununi  5659  fof  5806  f1ocnv  5840  isocnv  6239  isotr  6245  oprabid  6335  resiexg  6748  zfrep6  6780  ovmptss  6896  dmtpos  7003  tposfn  7020  smores  7089  omopthlem1  7374  eqer  7414  ixpeq2  7554  enssdom  7612  fiprc  7669  sbthlem9  7708  infensuc  7768  fipwuni  7958  zfreg  8128  zfreg2  8129  dfom3  8170  r1elss  8295  scott0  8375  fin56  8841  dominf  8893  ac6n  8933  brdom4  8976  dominfac  9016  inawina  9133  eltsk2g  9194  ltsosr  9536  ssxr  9721  recgt0ii  10534  sup2  10587  dfnn2  10644  peano2uz2  11046  eluzp1p1  11208  peano2uz  11235  zq  11293  ubmelfzo  12008  expclzlem  12334  wrdeq  12740  wwlktovf  13106  fsum2dlem  13908  fprod2dlem  14111  sin02gt0  14323  divalglem6  14457  qredeu  14743  isfunc  15847  xpcbas  16141  drsdirfi  16261  clatl  16440  tsrss  16547  gimcnv  17009  gsum2dlem1  17680  gsum2dlem2  17681  lmimcnv  18368  xrge0subm  19086  fctop  20096  cctop  20098  alexsubALTlem4  21143  lpbl  21596  xrge0gsumle  21929  xrge0tsms  21930  iirev  22035  iihalf1  22037  iihalf2  22039  iimulcl  22043  vitalilem1  22645  ply1idom  23152  aacjcl  23362  aannenlem2  23364  ang180lem4  23820  lgslem3  24305  axlowdim  25070  axcontlem2  25074  usgraexmplef  25207  nmobndseqi  26501  axhcompl-zf  26732  hhcmpl  26934  shunssi  27102  spansni  27291  pjoml3i  27320  cmcmlem  27325  nonbooli  27385  lnopco0i  27738  pjnmopi  27882  pjnormssi  27902  hatomistici  28096  cvexchi  28103  cmdmdi  28151  mddmdin0i  28165  cdj3lem3b  28174  disjin  28273  disjin2  28274  xrge0tsmsd  28622  issgon  29019  sxbrsigalem0  29166  eulerpartlemgs2  29286  ballotlem2  29394  ballotth  29443  ballotthOLD  29481  bnj945  29657  bnj556  29783  bnj557  29784  bnj607  29799  bnj864  29805  bnj969  29829  bnj999  29840  bnj1398  29915  elpotr  30498  dfon2lem8  30507  sltval2  30614  txpss3v  30716  meran1  31142  arg-ax  31147  bj-nfalt  31371  bj-eunex  31480  poimirlem25  32029  poimirlem30  32034  bndss  32182  fldcrng  32301  flddmn  32355  prter1  32515  mzpclall  35640  setindtrs  35951  dgraalem  36078  dgraalemOLD  36079  ifpimim  36224  inintabss  36255  refimssco  36284  cotrintab  36292  intimass  36317  psshepw  36455  nzin  36737  axc11next  36827  iotaexeu  36839  hbexgVD  37366  reuan  38746  aovpcov0  38837  aov0ov0  38840  enege  38920  onego  38921  gboagbo  39002  n0rex  39135  elfzlmr  39214  cusgrop  39670  rusgrpropedg  39789  mhmismgmhm  40314  sgrpplusgaopALT  40339  rhmisrnghm  40428  srhmsubclem1  40583  srhmsubcALTVlem1  40602  rhmsubcALTVlem3  40617  eluz2cnn0n1  40815  regt1loggt0  40855  rege1logbrege0  40877  rege1logbzge0  40878  relogbmulbexp  40880
  Copyright terms: Public domain W3C validator