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  1614  sbimi  1708  euanOLD  2339  ralimi2  2808  reximi2  2918  r19.28av  2952  r19.29r  2954  r19.30  2961  elex  3077  rmoan  3255  rmoimi2  3258  sseq2  3476  rabss2  3533  undif4  3833  r19.2zb  3868  ralf0  3884  difprsnss  4107  snsspw  4142  uniin  4209  intss  4247  iuniin  4279  iuneq1  4282  iuneq2  4285  iunpwss  4358  eunex  4583  rmorabex  4650  exss  4653  pwunss  4724  soeq2  4759  reliin  5059  coeq1  5095  coeq2  5096  cnveq  5111  dmeq  5138  dmin  5145  dmcoss  5197  rncoeq  5201  dminss  5349  imainss  5350  dfco2a  5436  iotaex  5496  fununi  5582  fof  5718  f1ocnv  5751  isocnv  6120  isotr  6126  oprabid  6214  resiexg  6614  zfrep6  6645  ovmptss  6754  dmtpos  6857  tposfn  6874  smores  6913  omopthlem1  7194  eqer  7234  ixpeq2  7377  enssdom  7434  fiprc  7491  sbthlem9  7529  infensuc  7589  fipwuni  7777  zfreg  7911  zfreg2  7912  dfom3  7954  r1elss  8114  scott0  8194  fin56  8663  dominf  8715  ac6n  8755  brdom4  8798  dominfac  8838  inawina  8958  eltsk2g  9019  ltsosr  9362  ssxr  9545  ltadd2i  9606  recgt0ii  10339  sup2  10387  dfnn2  10436  peano2uz2  10830  eluzp1p1  10987  peano2uz  11009  zq  11060  elfzmlbm  11591  ubmelfzo  11704  expclzlem  11990  wrdeq  12353  fsum2dlem  13339  sin02gt0  13578  divalglem6  13704  qredeu  13895  isfunc  14876  xpcbas  15090  drsdirfi  15210  clatl  15388  tsrss  15495  gimcnv  15897  gsum2dlem1  16566  gsum2dlem2  16567  gsum2dOLD  16569  lmimcnv  17254  xrge0subm  17963  fctop  18724  cctop  18726  alexsubALTlem4  19738  lpbl  20194  xrge0gsumle  20526  xrge0tsms  20527  iirev  20617  iihalf1  20619  iihalf2  20621  iimulcl  20625  vitalilem1  21204  itg2monolem1  21344  itg2monolem2  21345  itg2monolem3  21346  itg2mono  21347  itg2i1fseqle  21348  itg2i1fseq3  21351  itg2addlem  21352  itg2gt0  21354  itg2cnlem2  21356  ply1idom  21712  aacjcl  21909  aannenlem2  21911  ang180lem4  22324  lgslem3  22753  axlowdim  23342  axcontlem2  23346  usgraexmpl  23454  nmobndseqi  24314  axhcompl-zf  24535  hhcmpl  24737  shunssi  24906  spansni  25095  pjoml3i  25124  cmcmlem  25129  nonbooli  25189  lnopco0i  25543  pjnmopi  25687  pjnormssi  25707  hatomistici  25901  cvexchi  25908  cmdmdi  25956  mddmdin0i  25970  cdj3lem3b  25979  disjin  26063  xrge0tsmsd  26387  issgon  26700  sxbrsigalem0  26820  eulerpartlemgs2  26897  ballotlem2  27005  ballotth  27054  fprod2dlem  27625  elpotr  27728  dfon2lem8  27737  sltval2  27931  txpss3v  28043  meran1  28391  arg-ax  28396  itg2addnc  28584  itg2gt0cn  28585  ftc1anclem6  28610  ftc1anclem8  28612  bndss  28823  fldcrng  28942  flddmn  28996  prter1  29162  mzpclall  29201  setindtrs  29512  dgraalem  29640  axc11next  29798  iotaexeu  29810  reuan  30142  aovpcov0  30234  aov0ov0  30237  elopaelxp  30273  wwlktovf  30389  hbexgVD  31942  bnj945  32067  bnj556  32193  bnj557  32194  bnj607  32209  bnj864  32215  bnj969  32239  bnj999  32250  bnj1398  32325  bj-eunex  32620
  Copyright terms: Public domain W3C validator