MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr4i Structured version   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  1577  19.30  1614  sbimi  1664  nfimdOLD  1828  euan  2337  ralimi2  2770  reximi2  2804  r19.28av  2837  r19.29r  2839  r19.30  2845  elex  2956  rmoan  3124  rmoimi2  3127  sseq2  3362  rabss2  3418  undif4  3676  r19.2zb  3710  ralf0  3726  difprsnss  3926  snsspw  3962  uniin  4027  intss  4063  iuniin  4095  iuneq1  4098  iuneq2  4101  iunpwss  4172  eunex  4384  rmorabex  4415  exss  4418  pwunss  4480  soeq2  4515  reliin  4988  coeq1  5022  coeq2  5023  cnveq  5038  dmeq  5062  dmin  5069  dmcoss  5127  rncoeq  5131  resiexg  5180  dminss  5278  imainss  5279  dfco2a  5362  iotaex  5427  fununi  5509  fof  5645  f1ocnv  5679  zfrep6  5960  isocnv  6042  isotr  6048  oprabid  6097  ovmptss  6420  dmtpos  6483  tposfn  6500  smores  6606  omopthlem1  6890  eqer  6930  ixpeq2  7068  enssdom  7124  fiprc  7180  sbthlem9  7217  infensuc  7277  fipwuni  7423  zfreg  7555  zfreg2  7556  dfom3  7594  r1elss  7724  scott0  7802  fin56  8265  dominf  8317  ac6n  8357  brdom4  8400  dominfac  8440  inawina  8557  eltsk2g  8618  ltsosr  8961  ssxr  9137  ltadd2i  9196  recgt0ii  9908  sup2  9956  dfnn2  10005  peano2uz2  10349  eluzp1p1  10503  peano2uz  10522  zq  10572  expclzlem  11397  wrdeq  11730  fsum2dlem  12546  sin02gt0  12785  divalglem6  12910  qredeu  13099  isfunc  14053  xpcbas  14267  drsdirfi  14387  clatl  14535  tsrss  14647  gimcnv  15046  gsum2d  15538  lmimcnv  16131  xrge0subm  16731  fctop  17060  cctop  17062  alexsubALTlem4  18073  lpbl  18525  xrge0gsumle  18856  xrge0tsms  18857  iirev  18946  iihalf1  18948  iihalf2  18950  iimulcl  18954  vitalilem1  19492  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseqle  19638  itg2i1fseq3  19641  itg2addlem  19642  itg2gt0  19644  itg2cnlem2  19646  ply1idom  20039  aacjcl  20236  aannenlem2  20238  ang180lem4  20646  lgslem3  21074  usgraexmpl  21412  nmobndseqi  22272  axhcompl-zf  22493  hhcmpl  22694  shunssi  22862  spansni  23051  pjoml3i  23080  cmcmlem  23085  nonbooli  23145  lnopco0i  23499  pjnmopi  23643  pjnormssi  23663  hatomistici  23857  cvexchi  23864  cmdmdi  23912  mddmdin0i  23926  cdj3lem3b  23935  disjin  24019  xrge0tsmsd  24215  issgon  24498  sxbrsigalem0  24613  ballotlem2  24738  ballotth  24787  fprod2dlem  25296  elpotr  25400  dfon2lem8  25409  sltval2  25603  txpss3v  25715  axlowdim  25892  axcontlem2  25896  meran1  26153  arg-ax  26158  itg2addnc  26249  itg2gt0cn  26250  ftc1anclem6  26275  ftc1anclem8  26277  bndss  26486  fldcrng  26605  flddmn  26659  prter1  26719  mzpclall  26775  setindtrs  27087  dgraalem  27318  ax10ext  27574  iotaexeu  27586  reuan  27925  aovpcov0  28021  aov0ov0  28024  elfzmlbm  28090  hbexgVD  28955  bnj945  29081  bnj556  29208  bnj557  29209  bnj607  29224  bnj864  29230  bnj969  29254  bnj999  29265  bnj1398  29340
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