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, 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 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  1618  sbimi  1711  euanOLD  2335  ralimi2  2786  reximi2  2820  r19.28av  2854  r19.29r  2856  r19.30  2863  elex  2979  rmoan  3154  rmoimi2  3157  sseq2  3375  rabss2  3432  undif4  3732  r19.2zb  3767  ralf0  3783  difprsnss  4006  snsspw  4041  uniin  4108  intss  4146  iuniin  4178  iuneq1  4181  iuneq2  4184  iunpwss  4257  eunex  4482  rmorabex  4549  exss  4552  pwunss  4622  soeq2  4657  reliin  4957  coeq1  4993  coeq2  4994  cnveq  5009  dmeq  5036  dmin  5043  dmcoss  5095  rncoeq  5099  dminss  5248  imainss  5249  dfco2a  5335  iotaex  5395  fununi  5481  fof  5617  f1ocnv  5650  isocnv  6018  isotr  6024  oprabid  6114  resiexg  6513  zfrep6  6544  ovmptss  6653  dmtpos  6756  tposfn  6773  smores  6809  omopthlem1  7090  eqer  7130  ixpeq2  7273  enssdom  7330  fiprc  7387  sbthlem9  7425  infensuc  7485  fipwuni  7672  zfreg  7806  zfreg2  7807  dfom3  7849  r1elss  8009  scott0  8089  fin56  8558  dominf  8610  ac6n  8650  brdom4  8693  dominfac  8733  inawina  8853  eltsk2g  8914  ltsosr  9257  ssxr  9440  ltadd2i  9501  recgt0ii  10234  sup2  10282  dfnn2  10331  peano2uz2  10725  eluzp1p1  10882  peano2uz  10904  zq  10955  elfzmlbm  11486  ubmelfzo  11599  expclzlem  11885  wrdeq  12247  fsum2dlem  13233  sin02gt0  13472  divalglem6  13598  qredeu  13789  isfunc  14770  xpcbas  14984  drsdirfi  15104  clatl  15282  tsrss  15389  gimcnv  15788  gsum2dlem1  16451  gsum2dlem2  16452  gsum2dOLD  16454  lmimcnv  17126  xrge0subm  17813  fctop  18567  cctop  18569  alexsubALTlem4  19581  lpbl  20037  xrge0gsumle  20369  xrge0tsms  20370  iirev  20460  iihalf1  20462  iihalf2  20464  iimulcl  20468  vitalilem1  21047  itg2monolem1  21187  itg2monolem2  21188  itg2monolem3  21189  itg2mono  21190  itg2i1fseqle  21191  itg2i1fseq3  21194  itg2addlem  21195  itg2gt0  21197  itg2cnlem2  21199  ply1idom  21555  aacjcl  21752  aannenlem2  21754  ang180lem4  22167  lgslem3  22596  axlowdim  23142  axcontlem2  23146  usgraexmpl  23254  nmobndseqi  24114  axhcompl-zf  24335  hhcmpl  24537  shunssi  24706  spansni  24895  pjoml3i  24924  cmcmlem  24929  nonbooli  24989  lnopco0i  25343  pjnmopi  25487  pjnormssi  25507  hatomistici  25701  cvexchi  25708  cmdmdi  25756  mddmdin0i  25770  cdj3lem3b  25779  disjin  25864  xrge0tsmsd  26188  issgon  26502  sxbrsigalem0  26622  eulerpartlemgs2  26693  ballotlem2  26801  ballotth  26850  fprod2dlem  27420  elpotr  27523  dfon2lem8  27532  sltval2  27726  txpss3v  27838  meran1  28187  arg-ax  28192  itg2addnc  28371  itg2gt0cn  28372  ftc1anclem6  28397  ftc1anclem8  28399  bndss  28610  fldcrng  28729  flddmn  28783  prter1  28949  mzpclall  28988  setindtrs  29299  dgraalem  29427  axc11next  29585  iotaexeu  29597  reuan  29929  aovpcov0  30021  aov0ov0  30024  elopaelxp  30060  wwlktovf  30176  hbexgVD  31476  bnj945  31601  bnj556  31727  bnj557  31728  bnj607  31743  bnj864  31749  bnj969  31773  bnj999  31784  bnj1398  31859  bj-eunex  32080
  Copyright terms: Public domain W3C validator