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

Theorem 3imtr4i 258
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 188 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 204 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  hbxfrbi  1574  19.30  1611  sbimi  1659  nfimdOLD  1818  euan  2295  ralimi2  2721  reximi2  2755  r19.28av  2788  r19.29r  2790  r19.30  2796  elex  2907  rmoan  3075  rmoimi2  3078  sseq2  3313  rabss2  3369  undif4  3627  r19.2zb  3661  ralf0  3677  difprsnss  3877  snsspw  3912  uniin  3977  intss  4013  iuniin  4045  iuneq1  4048  iuneq2  4051  iunpwss  4121  eunex  4333  rmorabex  4364  exss  4367  pwunss  4429  soeq2  4464  reliin  4936  coeq1  4970  coeq2  4971  cnveq  4986  dmeq  5010  dmin  5017  dmcoss  5075  rncoeq  5079  resiexg  5128  dminss  5226  imainss  5227  dfco2a  5310  iotaex  5375  fununi  5457  fof  5593  f1ocnv  5627  zfrep6  5907  isocnv  5989  isotr  5995  oprabid  6044  ovmptss  6367  dmtpos  6427  tposfn  6444  smores  6550  omopthlem1  6834  eqer  6874  ixpeq2  7012  enssdom  7068  fiprc  7124  sbthlem9  7161  infensuc  7221  fipwuni  7366  zfreg  7496  zfreg2  7497  dfom3  7535  r1elss  7665  scott0  7743  fin56  8206  dominf  8258  ac6n  8298  brdom4  8341  dominfac  8381  inawina  8498  eltsk2g  8559  ltsosr  8902  ssxr  9078  ltadd2i  9136  recgt0ii  9848  sup2  9896  dfnn2  9945  peano2uz2  10289  eluzp1p1  10443  peano2uz  10462  zq  10512  expclzlem  11332  wrdeq  11665  fsum2dlem  12481  sin02gt0  12720  divalglem6  12845  qredeu  13034  isfunc  13988  xpcbas  14202  drsdirfi  14322  clatl  14470  tsrss  14582  gimcnv  14981  gsum2d  15473  lmimcnv  16066  xrge0subm  16662  fctop  16991  cctop  16993  alexsubALTlem4  18002  lpbl  18423  xrge0gsumle  18735  xrge0tsms  18736  iirev  18825  iihalf1  18827  iihalf2  18829  iimulcl  18833  vitalilem1  19367  itg2monolem1  19509  itg2monolem2  19510  itg2monolem3  19511  itg2mono  19512  itg2i1fseqle  19513  itg2i1fseq3  19516  itg2addlem  19517  itg2gt0  19519  itg2cnlem2  19521  ply1idom  19914  aacjcl  20111  aannenlem2  20113  ang180lem4  20521  lgslem3  20949  usgraexmpl  21286  nmobndseqi  22128  axhcompl-zf  22349  hhcmpl  22550  shunssi  22718  spansni  22907  pjoml3i  22936  cmcmlem  22941  nonbooli  23001  lnopco0i  23355  pjnmopi  23499  pjnormssi  23519  hatomistici  23713  cvexchi  23720  cmdmdi  23768  mddmdin0i  23782  cdj3lem3b  23791  disjin  23871  xrge0tsmsd  24052  issgon  24302  sxbrsigalem0  24415  ballotlem2  24525  ballotth  24574  elpotr  25161  dfon2lem8  25170  sltval2  25334  txpss3v  25442  limitssson  25475  axlowdim  25614  axcontlem2  25618  meran1  25875  arg-ax  25880  itg2gt0cn  25960  bndss  26186  fldcrng  26305  flddmn  26359  prter1  26419  mzpclall  26475  setindtrs  26787  dgraalem  27019  ax10ext  27275  iotaexeu  27287  reuan  27626  aovpcov0  27723  aov0ov0  27726  hbexgVD  28359  bnj945  28482  bnj556  28609  bnj557  28610  bnj607  28625  bnj864  28631  bnj969  28655  bnj999  28666  bnj1398  28741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator