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

Theorem 3imtr4i 258
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 188 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 204 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  hbxfrbi  1574  19.30  1611  sbimi  1660  nfimdOLD  1824  euan  2311  ralimi2  2738  reximi2  2772  r19.28av  2805  r19.29r  2807  r19.30  2813  elex  2924  rmoan  3092  rmoimi2  3095  sseq2  3330  rabss2  3386  undif4  3644  r19.2zb  3678  ralf0  3694  difprsnss  3894  snsspw  3930  uniin  3995  intss  4031  iuniin  4063  iuneq1  4066  iuneq2  4069  iunpwss  4140  eunex  4352  rmorabex  4383  exss  4386  pwunss  4448  soeq2  4483  reliin  4955  coeq1  4989  coeq2  4990  cnveq  5005  dmeq  5029  dmin  5036  dmcoss  5094  rncoeq  5098  resiexg  5147  dminss  5245  imainss  5246  dfco2a  5329  iotaex  5394  fununi  5476  fof  5612  f1ocnv  5646  zfrep6  5927  isocnv  6009  isotr  6015  oprabid  6064  ovmptss  6387  dmtpos  6450  tposfn  6467  smores  6573  omopthlem1  6857  eqer  6897  ixpeq2  7035  enssdom  7091  fiprc  7147  sbthlem9  7184  infensuc  7244  fipwuni  7389  zfreg  7519  zfreg2  7520  dfom3  7558  r1elss  7688  scott0  7766  fin56  8229  dominf  8281  ac6n  8321  brdom4  8364  dominfac  8404  inawina  8521  eltsk2g  8582  ltsosr  8925  ssxr  9101  ltadd2i  9160  recgt0ii  9872  sup2  9920  dfnn2  9969  peano2uz2  10313  eluzp1p1  10467  peano2uz  10486  zq  10536  expclzlem  11360  wrdeq  11693  fsum2dlem  12509  sin02gt0  12748  divalglem6  12873  qredeu  13062  isfunc  14016  xpcbas  14230  drsdirfi  14350  clatl  14498  tsrss  14610  gimcnv  15009  gsum2d  15501  lmimcnv  16094  xrge0subm  16694  fctop  17023  cctop  17025  alexsubALTlem4  18034  lpbl  18486  xrge0gsumle  18817  xrge0tsms  18818  iirev  18907  iihalf1  18909  iihalf2  18911  iimulcl  18915  vitalilem1  19453  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq3  19602  itg2addlem  19603  itg2gt0  19605  itg2cnlem2  19607  ply1idom  20000  aacjcl  20197  aannenlem2  20199  ang180lem4  20607  lgslem3  21035  usgraexmpl  21373  nmobndseqi  22233  axhcompl-zf  22454  hhcmpl  22655  shunssi  22823  spansni  23012  pjoml3i  23041  cmcmlem  23046  nonbooli  23106  lnopco0i  23460  pjnmopi  23604  pjnormssi  23624  hatomistici  23818  cvexchi  23825  cmdmdi  23873  mddmdin0i  23887  cdj3lem3b  23896  disjin  23980  xrge0tsmsd  24176  issgon  24459  sxbrsigalem0  24574  ballotlem2  24699  ballotth  24748  fprod2dlem  25257  elpotr  25351  dfon2lem8  25360  sltval2  25524  txpss3v  25632  limitssson  25665  axlowdim  25804  axcontlem2  25808  meran1  26065  arg-ax  26070  itg2addnc  26158  itg2gt0cn  26159  bndss  26385  fldcrng  26504  flddmn  26558  prter1  26618  mzpclall  26674  setindtrs  26986  dgraalem  27218  ax10ext  27474  iotaexeu  27486  reuan  27825  aovpcov0  27921  aov0ov0  27924  elfzmlbm  27977  hbexgVD  28727  bnj945  28850  bnj556  28977  bnj557  28978  bnj607  28993  bnj864  28999  bnj969  29023  bnj999  29034  bnj1398  29109
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 178
  Copyright terms: Public domain W3C validator