MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr4i Structured version   Visualization 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  1696  sbimi  1805  ralimi2  2780  reximi2  2856  r19.28v  2926  r19.29r  2928  r19.30  2937  elex  3056  rmoan  3240  rmoimi2  3243  sseq2  3456  rabss2  3514  undif4  3823  r19.2zb  3861  ralf0  3878  difprsnss  4110  snsspw  4146  uniin  4221  intssOLD  4259  iuniin  4292  iuneq1  4295  iuneq2  4298  iunpwss  4374  eunex  4599  rmorabex  4663  exss  4666  pwunss  4742  soeq2  4778  elopaelxp  4910  reliin  4958  coeq1  4995  coeq2  4996  cnveq  5011  dmeq  5038  dmin  5045  dmcoss  5097  rncoeq  5101  dminss  5253  imainss  5254  dfco2a  5338  iotaex  5566  fununi  5654  fof  5798  f1ocnv  5831  isocnv  6226  isotr  6232  oprabid  6322  resiexg  6734  zfrep6  6766  ovmptss  6882  dmtpos  6990  tposfn  7007  smores  7076  omopthlem1  7361  eqer  7401  ixpeq2  7541  enssdom  7599  fiprc  7656  sbthlem9  7695  infensuc  7755  fipwuni  7945  zfreg  8115  zfreg2  8116  dfom3  8157  r1elss  8282  scott0  8362  fin56  8828  dominf  8880  ac6n  8920  brdom4  8963  dominfac  9003  inawina  9120  eltsk2g  9181  ltsosr  9523  ssxr  9708  ltadd2iOLD  9771  recgt0ii  10519  sup2  10572  dfnn2  10629  peano2uz2  11030  eluzp1p1  11191  peano2uz  11219  zq  11277  elfzmlbmOLD  11908  ubmelfzo  11986  expclzlem  12303  wrdeq  12696  wwlktovf  13043  fsum2dlem  13843  fprod2dlem  14046  sin02gt0  14258  divalglem6  14390  qredeu  14676  isfunc  15781  xpcbas  16075  drsdirfi  16195  clatl  16374  tsrss  16481  gimcnv  16943  gsum2dlem1  17614  gsum2dlem2  17615  lmimcnv  18302  xrge0subm  19021  fctop  20031  cctop  20033  alexsubALTlem4  21077  lpbl  21530  xrge0gsumle  21863  xrge0tsms  21864  iirev  21969  iihalf1  21971  iihalf2  21973  iimulcl  21977  vitalilem1  22578  ply1idom  23085  aacjcl  23295  aannenlem2  23297  ang180lem4  23753  lgslem3  24238  axlowdim  25003  axcontlem2  25007  usgraexmplef  25140  nmobndseqi  26432  axhcompl-zf  26663  hhcmpl  26865  shunssi  27033  spansni  27222  pjoml3i  27251  cmcmlem  27256  nonbooli  27316  lnopco0i  27669  pjnmopi  27813  pjnormssi  27833  hatomistici  28027  cvexchi  28034  cmdmdi  28082  mddmdin0i  28096  cdj3lem3b  28105  disjin  28208  disjin2  28209  xrge0tsmsd  28560  issgon  28957  sxbrsigalem0  29105  eulerpartlemgs2  29225  ballotlem2  29333  ballotth  29382  ballotthOLD  29420  bnj945  29597  bnj556  29723  bnj557  29724  bnj607  29739  bnj864  29745  bnj969  29769  bnj999  29780  bnj1398  29855  elpotr  30439  dfon2lem8  30448  sltval2  30555  txpss3v  30657  meran1  31083  arg-ax  31088  bj-nfalt  31317  bj-eunex  31426  poimirlem25  31977  poimirlem30  31982  bndss  32130  fldcrng  32249  flddmn  32303  prter1  32463  mzpclall  35581  setindtrs  35892  dgraalem  36019  dgraalemOLD  36020  ifpimim  36165  inintabss  36196  refimssco  36225  cotrintab  36233  intimass  36258  psshepw  36396  nzin  36678  axc11next  36768  iotaexeu  36780  hbexgVD  37313  reuan  38611  aovpcov0  38702  aov0ov0  38705  enege  38785  onego  38786  gboagbo  38867  n0rex  38998  cusgrop  39515  rusgrpropedg  39610  mhmismgmhm  39910  sgrpplusgaopALT  39935  rhmisrnghm  40024  srhmsubclem1  40179  srhmsubcALTVlem1  40198  rhmsubcALTVlem3  40213  eluz2cnn0n1  40411  regt1loggt0  40451  rege1logbrege0  40473  rege1logbzge0  40474  relogbmulbexp  40476
  Copyright terms: Public domain W3C validator