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

Theorem 3imtr4i 266
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 195 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 212 1  |-  ( ch 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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
This theorem is referenced by:  hbxfrbi  1664  sbimi  1769  ralimi2  2793  reximi2  2870  r19.28v  2940  r19.29r  2942  r19.30  2951  elex  3067  rmoan  3247  rmoimi2  3250  sseq2  3463  rabss2  3521  undif4  3825  r19.2zb  3862  ralf0  3879  difprsnss  4106  snsspw  4142  uniin  4210  intssOLD  4248  iuniin  4281  iuneq1  4284  iuneq2  4287  iunpwss  4363  eunex  4586  rmorabex  4650  exss  4653  pwunss  4727  soeq2  4763  elopaelxp  4895  reliin  4943  coeq1  4980  coeq2  4981  cnveq  4996  dmeq  5023  dmin  5030  dmcoss  5082  rncoeq  5086  dminss  5237  imainss  5238  dfco2a  5322  iotaex  5549  fununi  5634  fof  5777  f1ocnv  5810  isocnv  6208  isotr  6214  oprabid  6304  resiexg  6719  zfrep6  6751  ovmptss  6864  dmtpos  6969  tposfn  6986  smores  7055  omopthlem1  7340  eqer  7380  ixpeq2  7520  enssdom  7577  fiprc  7634  sbthlem9  7672  infensuc  7732  fipwuni  7919  zfreg  8054  zfreg2  8055  dfom3  8096  r1elss  8255  scott0  8335  fin56  8804  dominf  8856  ac6n  8896  brdom4  8939  dominfac  8979  inawina  9097  eltsk2g  9158  ltsosr  9500  ssxr  9684  ltadd2iOLD  9747  recgt0ii  10490  sup2  10538  dfnn2  10588  peano2uz2  10990  eluzp1p1  11151  peano2uz  11179  zq  11232  elfzmlbmOLD  11838  ubmelfzo  11915  expclzlem  12232  wrdeq  12614  wwlktovf  12948  fsum2dlem  13734  fprod2dlem  13934  sin02gt0  14134  divalglem6  14263  qredeu  14455  isfunc  15475  xpcbas  15769  drsdirfi  15889  clatl  16068  tsrss  16175  gimcnv  16637  gsum2dlem1  17316  gsum2dlem2  17317  gsum2dOLD  17319  lmimcnv  18031  xrge0subm  18777  fctop  19795  cctop  19797  alexsubALTlem4  20840  lpbl  21296  xrge0gsumle  21628  xrge0tsms  21629  iirev  21719  iihalf1  21721  iihalf2  21723  iimulcl  21727  vitalilem1  22307  ply1idom  22815  aacjcl  23013  aannenlem2  23015  ang180lem4  23469  lgslem3  23952  axlowdim  24668  axcontlem2  24672  usgraexmpl  24805  nmobndseqi  26094  axhcompl-zf  26315  hhcmpl  26517  shunssi  26686  spansni  26875  pjoml3i  26904  cmcmlem  26909  nonbooli  26969  lnopco0i  27322  pjnmopi  27466  pjnormssi  27486  hatomistici  27680  cvexchi  27687  cmdmdi  27735  mddmdin0i  27749  cdj3lem3b  27758  disjin  27864  disjin2  27865  xrge0tsmsd  28214  issgon  28557  sxbrsigalem0  28705  eulerpartlemgs2  28811  ballotlem2  28919  ballotth  28968  bnj945  29146  bnj556  29272  bnj557  29273  bnj607  29288  bnj864  29294  bnj969  29318  bnj999  29329  bnj1398  29404  elpotr  29987  dfon2lem8  29996  sltval2  30103  txpss3v  30203  meran1  30630  arg-ax  30635  bj-nfalt  30816  bj-eunex  30936  bndss  31544  fldcrng  31663  flddmn  31717  prter1  31882  mzpclall  35001  setindtrs  35309  dgraalem  35438  ifpimim  35580  intimass  35613  psshepw  35749  nzin  36051  axc11next  36141  iotaexeu  36153  hbexgVD  36717  reuan  37534  aovpcov0  37624  aov0ov0  37627  enege  37709  onego  37710  gboagbo  37791  mhmismgmhm  38104  sgrpplusgaopALT  38129  rhmisrnghm  38218  srhmsubclem1  38373  srhmsubcALTVlem1  38392  rhmsubcALTVlem3  38407  eluz2cnn0n1  38607  regt1loggt0  38648  rege1logbrege0  38670  rege1logbzge0  38671  relogbmulbexp  38673
  Copyright terms: Public domain W3C validator