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  1558  19.30  1594  sbimi  1642  nfimd  1773  euan  2213  ralimi2  2628  reximi2  2662  r19.28av  2695  r19.29r  2697  r19.30  2698  elex  2809  rmoan  2976  rmoimi2  2979  sseq2  3213  rabss2  3269  undif4  3524  r19.2zb  3557  ralf0  3573  difprsnss  3769  snsspw  3800  uniin  3863  intss  3899  iuniin  3931  iuneq1  3934  iuneq2  3937  iunpwss  4007  eunex  4219  rmorabex  4249  exss  4252  pwunss  4314  soeq2  4350  reliin  4823  coeq1  4857  coeq2  4858  cnveq  4871  dmeq  4895  dmin  4902  dmcoss  4960  rncoeq  4964  resiexg  5013  dminss  5111  imainss  5112  dfco2a  5189  iotaex  5252  fununi  5332  fof  5467  f1ocnv  5501  zfrep6  5764  isocnv  5843  isotr  5849  oprabid  5898  ovmptss  6216  dmtpos  6262  tposfn  6279  smores  6385  omopthlem1  6669  eqer  6709  ixpeq2  6846  enssdom  6902  fiprc  6958  sbthlem9  6995  infensuc  7055  fipwuni  7195  zfreg  7325  zfreg2  7326  dfom3  7364  r1elss  7494  scott0  7572  fin56  8035  dominf  8087  ac6n  8128  brdom4  8171  dominfac  8211  inawina  8328  eltsk2g  8389  ltsosr  8732  ssxr  8908  ltadd2i  8966  recgt0ii  9678  sup2  9726  dfnn2  9775  peano2uz2  10115  eluzp1p1  10269  peano2uz  10288  zq  10338  expclzlem  11143  wrdeq  11440  fsum2dlem  12249  sin02gt0  12488  divalglem6  12613  qredeu  12802  isfunc  13754  xpcbas  13968  drsdirfi  14088  clatl  14236  tsrss  14348  gimcnv  14747  gsum2d  15239  lmimcnv  15836  xrge0subm  16428  fctop  16757  cctop  16759  alexsubALTlem4  17760  lpbl  18065  xrge0gsumle  18354  xrge0tsms  18355  iirev  18443  iihalf1  18445  iihalf2  18447  iimulcl  18451  vitalilem1  18979  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq3  19128  itg2addlem  19129  itg2gt0  19131  itg2cnlem2  19133  ply1idom  19526  aacjcl  19723  aannenlem2  19725  ang180lem4  20126  lgslem3  20553  nmobndseqi  21373  axhcompl-zf  21594  hhcmpl  21795  shunssi  21963  spansni  22152  pjoml3i  22181  cmcmlem  22186  nonbooli  22246  lnopco0i  22600  pjnmopi  22744  pjnormssi  22764  hatomistici  22958  cvexchi  22965  cmdmdi  23013  mddmdin0i  23027  cdj3lem3b  23036  ballotth  23112  disjin  23377  xrge0tsmsd  23397  issgon  23499  elpotr  24208  dfon2lem8  24217  sltval2  24381  txpss3v  24489  limitssson  24522  axlowdim  24661  axcontlem2  24665  meran1  24922  arg-ax  24927  itg2gt0cn  25006  diaimi  25091  evpexun  25101  dstr  25274  tolat  25389  latdir  25398  ablocomgrp  25445  claddrvr  25751  rnegvex2  25764  negveudr  25772  clsmulrv  25786  divclrvd  25798  bndss  26613  fldcrng  26732  flddmn  26786  prter1  26850  mzpclall  26908  setindtrs  27221  dgraalem  27453  ax10ext  27709  iotaexeu  27721  stoweidlem14  27866  reuan  28061  aovpcov0  28158  aov0ov0  28161  usgraexmpl  28267  hbexgVD  28998  bnj945  29121  bnj556  29248  bnj557  29249  bnj607  29264  bnj864  29270  bnj969  29294  bnj999  29305
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