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

Theorem 3imtr4i 270
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 199 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 216 1  |-  ( ch 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  hbxfrbi  1691  sbimi  1793  ralimi2  2816  reximi2  2893  r19.28v  2963  r19.29r  2965  r19.30  2974  elex  3091  rmoan  3271  rmoimi2  3274  sseq2  3487  rabss2  3545  undif4  3850  r19.2zb  3888  ralf0  3905  difprsnss  4133  snsspw  4169  uniin  4237  intssOLD  4275  iuniin  4308  iuneq1  4311  iuneq2  4314  iunpwss  4390  eunex  4615  rmorabex  4679  exss  4682  pwunss  4756  soeq2  4792  elopaelxp  4924  reliin  4972  coeq1  5009  coeq2  5010  cnveq  5025  dmeq  5052  dmin  5059  dmcoss  5111  rncoeq  5115  dminss  5267  imainss  5268  dfco2a  5352  iotaex  5580  fununi  5665  fof  5808  f1ocnv  5841  isocnv  6234  isotr  6240  oprabid  6330  resiexg  6741  zfrep6  6773  ovmptss  6886  dmtpos  6991  tposfn  7008  smores  7077  omopthlem1  7362  eqer  7402  ixpeq2  7542  enssdom  7599  fiprc  7656  sbthlem9  7694  infensuc  7754  fipwuni  7944  zfreg  8114  zfreg2  8115  dfom3  8156  r1elss  8280  scott0  8360  fin56  8825  dominf  8877  ac6n  8917  brdom4  8960  dominfac  9000  inawina  9117  eltsk2g  9178  ltsosr  9520  ssxr  9705  ltadd2iOLD  9768  recgt0ii  10514  sup2  10567  dfnn2  10624  peano2uz2  11025  eluzp1p1  11186  peano2uz  11214  zq  11272  elfzmlbmOLD  11903  ubmelfzo  11980  expclzlem  12297  wrdeq  12687  wwlktovf  13025  fsum2dlem  13824  fprod2dlem  14027  sin02gt0  14239  divalglem6  14371  qredeu  14657  isfunc  15762  xpcbas  16056  drsdirfi  16176  clatl  16355  tsrss  16462  gimcnv  16924  gsum2dlem1  17595  gsum2dlem2  17596  lmimcnv  18283  xrge0subm  19002  fctop  20011  cctop  20013  alexsubALTlem4  21057  lpbl  21510  xrge0gsumle  21843  xrge0tsms  21844  iirev  21949  iihalf1  21951  iihalf2  21953  iimulcl  21957  vitalilem1  22558  ply1idom  23065  aacjcl  23275  aannenlem2  23277  ang180lem4  23733  lgslem3  24218  axlowdim  24983  axcontlem2  24987  usgraexmplef  25120  nmobndseqi  26412  axhcompl-zf  26643  hhcmpl  26845  shunssi  27013  spansni  27202  pjoml3i  27231  cmcmlem  27236  nonbooli  27296  lnopco0i  27649  pjnmopi  27793  pjnormssi  27813  hatomistici  28007  cvexchi  28014  cmdmdi  28062  mddmdin0i  28076  cdj3lem3b  28085  disjin  28192  disjin2  28193  xrge0tsmsd  28550  issgon  28947  sxbrsigalem0  29095  eulerpartlemgs2  29215  ballotlem2  29323  ballotth  29372  ballotthOLD  29410  bnj945  29587  bnj556  29713  bnj557  29714  bnj607  29729  bnj864  29735  bnj969  29759  bnj999  29770  bnj1398  29845  elpotr  30428  dfon2lem8  30437  sltval2  30544  txpss3v  30644  meran1  31070  arg-ax  31075  bj-nfalt  31259  bj-eunex  31378  poimirlem25  31923  poimirlem30  31928  bndss  32076  fldcrng  32195  flddmn  32249  prter1  32413  mzpclall  35532  setindtrs  35844  dgraalem  35971  dgraalemOLD  35972  ifpimim  36117  intimass  36150  psshepw  36286  nzin  36569  axc11next  36659  iotaexeu  36671  hbexgVD  37208  reuan  38358  aovpcov0  38448  aov0ov0  38451  enege  38531  onego  38532  gboagbo  38613  mhmismgmhm  39148  sgrpplusgaopALT  39173  rhmisrnghm  39262  srhmsubclem1  39417  srhmsubcALTVlem1  39436  rhmsubcALTVlem3  39451  eluz2cnn0n1  39651  regt1loggt0  39691  rege1logbrege0  39713  rege1logbzge0  39714  relogbmulbexp  39716
  Copyright terms: Public domain W3C validator