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  1644  sbimi  1746  ralimi2  2847  reximi2  2924  r19.28v  2991  r19.29r  2993  r19.30  3002  elex  3118  rmoan  3298  rmoimi2  3301  sseq2  3521  rabss2  3579  undif4  3886  r19.2zb  3922  ralf0  3939  difprsnss  4167  snsspw  4203  uniin  4271  intssOLD  4310  iuniin  4343  iuneq1  4346  iuneq2  4349  iunpwss  4425  eunex  4649  rmorabex  4716  exss  4719  pwunss  4794  soeq2  4829  elopaelxp  5081  reliin  5133  coeq1  5170  coeq2  5171  cnveq  5186  dmeq  5213  dmin  5220  dmcoss  5272  rncoeq  5276  dminss  5427  imainss  5428  dfco2a  5513  iotaex  5574  fununi  5660  fof  5801  f1ocnv  5834  isocnv  6227  isotr  6233  oprabid  6323  resiexg  6735  zfrep6  6767  ovmptss  6880  dmtpos  6985  tposfn  7002  smores  7041  omopthlem1  7322  eqer  7362  ixpeq2  7502  enssdom  7559  fiprc  7616  sbthlem9  7654  infensuc  7714  fipwuni  7904  zfreg  8039  zfreg2  8040  dfom3  8081  r1elss  8241  scott0  8321  fin56  8790  dominf  8842  ac6n  8882  brdom4  8925  dominfac  8965  inawina  9085  eltsk2g  9146  ltsosr  9488  ssxr  9671  ltadd2iOLD  9733  recgt0ii  10471  sup2  10519  dfnn2  10569  peano2uz2  10971  eluzp1p1  11131  peano2uz  11159  zq  11213  elfzmlbmOLD  11810  ubmelfzo  11883  expclzlem  12192  wrdeq  12570  wwlktovf  12905  fsum2dlem  13596  fprod2dlem  13795  sin02gt0  13938  divalglem6  14067  qredeu  14259  isfunc  15279  xpcbas  15573  drsdirfi  15693  clatl  15872  tsrss  15979  gimcnv  16441  gsum2dlem1  17123  gsum2dlem2  17124  gsum2dOLD  17126  lmimcnv  17839  xrge0subm  18585  fctop  19631  cctop  19633  alexsubALTlem4  20675  lpbl  21131  xrge0gsumle  21463  xrge0tsms  21464  iirev  21554  iihalf1  21556  iihalf2  21558  iimulcl  21562  vitalilem1  22142  ply1idom  22650  aacjcl  22848  aannenlem2  22850  ang180lem4  23269  lgslem3  23698  axlowdim  24390  axcontlem2  24394  usgraexmpl  24527  nmobndseqi  25820  axhcompl-zf  26041  hhcmpl  26243  shunssi  26412  spansni  26601  pjoml3i  26630  cmcmlem  26635  nonbooli  26695  lnopco0i  27049  pjnmopi  27193  pjnormssi  27213  hatomistici  27407  cvexchi  27414  cmdmdi  27462  mddmdin0i  27476  cdj3lem3b  27485  disjin  27583  xrge0tsmsd  27928  issgon  28284  sxbrsigalem0  28403  eulerpartlemgs2  28494  ballotlem2  28602  ballotth  28651  elpotr  29387  dfon2lem8  29396  sltval2  29590  txpss3v  29690  meran1  30038  arg-ax  30043  bndss  30444  fldcrng  30563  flddmn  30617  prter1  30782  mzpclall  30821  setindtrs  31129  dgraalem  31256  nzin  31385  axc11next  31475  iotaexeu  31487  reuan  32346  aovpcov0  32436  aov0ov0  32439  mhmismgmhm  32714  sgrpplusgaopALT  32739  rhmisrnghm  32828  srhmsubclem1  32983  srhmsubcOLDlem1  33002  rhmsubcOLDlem3  33017  hbexgVD  33807  bnj945  33933  bnj556  34059  bnj557  34060  bnj607  34075  bnj864  34081  bnj969  34105  bnj999  34116  bnj1398  34191  bj-nfalt  34366  bj-eunex  34486  bj-ifimim  37817  intimass  37869  psshepw  37912
  Copyright terms: Public domain W3C validator