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

Theorem 3imtr4i 257
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-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 187 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 203 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  hbxfrbi  1555  19.30  1591  sbimi  1633  nfimd  1761  euan  2200  ralimi2  2615  reximi2  2649  r19.28av  2682  r19.29r  2684  r19.30  2685  elex  2796  rmoan  2963  rmoimi2  2966  sseq2  3200  rabss2  3256  undif4  3511  r19.2zb  3544  ralf0  3560  difprsn  3756  snsspw  3784  uniin  3847  intss  3883  iuniin  3915  iuneq1  3918  iuneq2  3921  iunpwss  3991  eunex  4203  rmorabex  4233  exss  4236  pwunss  4298  soeq2  4334  reliin  4807  coeq1  4841  coeq2  4842  cnveq  4855  dmeq  4879  dmin  4886  dmcoss  4944  rncoeq  4948  resiexg  4997  dminss  5095  imainss  5096  dfco2a  5173  iotaex  5236  fununi  5316  fof  5451  f1ocnv  5485  zfrep6  5748  isocnv  5827  isotr  5833  oprabid  5882  ovmptss  6200  dmtpos  6246  tposfn  6263  smores  6369  omopthlem1  6653  eqer  6693  ixpeq2  6830  enssdom  6886  fiprc  6942  sbthlem9  6979  infensuc  7039  fipwuni  7179  zfreg  7309  zfreg2  7310  dfom3  7348  r1elss  7478  scott0  7556  fin56  8019  dominf  8071  ac6n  8112  brdom4  8155  dominfac  8195  inawina  8312  eltsk2g  8373  ltsosr  8716  ssxr  8892  ltadd2i  8950  recgt0ii  9662  sup2  9710  dfnn2  9759  peano2uz2  10099  eluzp1p1  10253  peano2uz  10272  zq  10322  expclzlem  11127  wrdeq  11424  fsum2dlem  12233  sin02gt0  12472  divalglem6  12597  qredeu  12786  isfunc  13738  xpcbas  13952  drsdirfi  14072  clatl  14220  tsrss  14332  gimcnv  14731  gsum2d  15223  lmimcnv  15820  xrge0subm  16412  fctop  16741  cctop  16743  alexsubALTlem4  17744  lpbl  18049  xrge0gsumle  18338  xrge0tsms  18339  iirev  18427  iihalf1  18429  iihalf2  18431  iimulcl  18435  vitalilem1  18963  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq3  19112  itg2addlem  19113  itg2gt0  19115  itg2cnlem2  19117  ply1idom  19510  aacjcl  19707  aannenlem2  19709  ang180lem4  20110  lgslem3  20537  nmobndseqi  21357  axhcompl-zf  21578  hhcmpl  21779  shunssi  21947  spansni  22136  pjoml3i  22165  cmcmlem  22170  nonbooli  22230  lnopco0i  22584  pjnmopi  22728  pjnormssi  22748  hatomistici  22942  cvexchi  22949  cmdmdi  22997  mddmdin0i  23011  cdj3lem3b  23020  ballotth  23096  disjin  23362  xrge0tsmsd  23382  issgon  23484  elpotr  24137  dfon2lem8  24146  sltval2  24310  txpss3v  24418  limitssson  24451  axlowdim  24589  axcontlem2  24593  meran1  24850  arg-ax  24855  diaimi  24988  evpexun  24998  dstr  25171  tolat  25286  latdir  25295  ablocomgrp  25342  claddrvr  25648  rnegvex2  25661  negveudr  25669  clsmulrv  25683  divclrvd  25695  bndss  26510  fldcrng  26629  flddmn  26683  prter1  26747  mzpclall  26805  setindtrs  27118  dgraalem  27350  ax10ext  27606  iotaexeu  27618  stoweidlem14  27763  reuan  27958  aovpcov0  28050  aov0ov0  28053  usgraexmpl  28133  hbexgVD  28682  bnj945  28805  bnj556  28932  bnj557  28933  bnj607  28948  bnj864  28954  bnj969  28978  bnj999  28989
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator