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

Theorem 3imtr4i 266
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 195 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 212 1  |-  ( ch 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  hbxfrbi  1623  sbimi  1717  euanOLD  2354  ralimi2  2854  reximi2  2931  r19.28av  2996  r19.29r  2998  r19.30  3006  elex  3122  rmoan  3302  rmoimi2  3305  sseq2  3526  rabss2  3583  undif4  3883  r19.2zb  3918  ralf0  3934  difprsnss  4162  snsspw  4198  uniin  4265  intss  4303  iuniin  4336  iuneq1  4339  iuneq2  4342  iunpwss  4415  eunex  4640  rmorabex  4707  exss  4710  pwunss  4785  soeq2  4820  elopaelxp  5071  reliin  5122  coeq1  5158  coeq2  5159  cnveq  5174  dmeq  5201  dmin  5208  dmcoss  5260  rncoeq  5264  dminss  5418  imainss  5419  dfco2a  5505  iotaex  5566  fununi  5652  fof  5793  f1ocnv  5826  isocnv  6212  isotr  6218  oprabid  6306  resiexg  6717  zfrep6  6749  ovmptss  6861  dmtpos  6964  tposfn  6981  smores  7020  omopthlem1  7301  eqer  7341  ixpeq2  7480  enssdom  7537  fiprc  7594  sbthlem9  7632  infensuc  7692  fipwuni  7882  zfreg  8017  zfreg2  8018  dfom3  8060  r1elss  8220  scott0  8300  fin56  8769  dominf  8821  ac6n  8861  brdom4  8904  dominfac  8944  inawina  9064  eltsk2g  9125  ltsosr  9467  ssxr  9650  ltadd2i  9711  recgt0ii  10447  sup2  10495  dfnn2  10545  peano2uz2  10944  eluzp1p1  11103  peano2uz  11130  zq  11184  elfzmlbm  11778  ubmelfzo  11845  expclzlem  12153  wrdeq  12524  wwlktovf  12851  fsum2dlem  13541  sin02gt0  13781  divalglem6  13908  qredeu  14100  isfunc  15084  xpcbas  15298  drsdirfi  15418  clatl  15596  tsrss  15703  gimcnv  16107  gsum2dlem1  16785  gsum2dlem2  16786  gsum2dOLD  16788  lmimcnv  17493  xrge0subm  18224  fctop  19268  cctop  19270  alexsubALTlem4  20282  lpbl  20738  xrge0gsumle  21070  xrge0tsms  21071  iirev  21161  iihalf1  21163  iihalf2  21165  iimulcl  21169  vitalilem1  21749  itg2monolem1  21889  itg2monolem2  21890  itg2monolem3  21891  itg2mono  21892  itg2i1fseqle  21893  itg2i1fseq3  21896  itg2addlem  21897  itg2gt0  21899  itg2cnlem2  21901  ply1idom  22257  aacjcl  22454  aannenlem2  22456  ang180lem4  22869  lgslem3  23298  axlowdim  23937  axcontlem2  23941  usgraexmpl  24074  nmobndseqi  25367  axhcompl-zf  25588  hhcmpl  25790  shunssi  25959  spansni  26148  pjoml3i  26177  cmcmlem  26182  nonbooli  26242  lnopco0i  26596  pjnmopi  26740  pjnormssi  26760  hatomistici  26954  cvexchi  26961  cmdmdi  27009  mddmdin0i  27023  cdj3lem3b  27032  disjin  27116  xrge0tsmsd  27435  issgon  27760  sxbrsigalem0  27879  eulerpartlemgs2  27956  ballotlem2  28064  ballotth  28113  fprod2dlem  28684  elpotr  28787  dfon2lem8  28796  sltval2  28990  txpss3v  29102  meran1  29450  arg-ax  29455  itg2addnc  29644  itg2gt0cn  29645  ftc1anclem6  29670  ftc1anclem8  29672  bndss  29883  fldcrng  30002  flddmn  30056  prter1  30222  mzpclall  30261  setindtrs  30571  dgraalem  30699  nzin  30823  axc11next  30891  iotaexeu  30903  reuan  31652  aovpcov0  31742  aov0ov0  31745  sgrpplusgaopALT  31943  hbexgVD  32786  bnj945  32911  bnj556  33037  bnj557  33038  bnj607  33053  bnj864  33059  bnj969  33083  bnj999  33094  bnj1398  33169  bj-eunex  33466
  Copyright terms: Public domain W3C validator