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

Theorem 3imtr4g 261
Description: More general version of 3imtr4i 257. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypotheses
Ref Expression
3imtr4g.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr4g.2  |-  ( th  <->  ps )
3imtr4g.3  |-  ( ta  <->  ch )
Assertion
Ref Expression
3imtr4g  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3  |-  ( th  <->  ps )
2 3imtr4g.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5bi 208 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 218 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3anim123d  1259  3orim123d  1260  moim  2202  morimv  2204  2euswap  2232  ralim  2627  ralimdaa  2633  ralimdv2  2636  rexim  2660  reximdv2  2665  moeq3  2955  rmoim  2977  2reuswap  2980  ssel  3187  sstr2  3199  sscon  3323  ssdif  3324  unss1  3357  ssrin  3407  difin0ss  3533  r19.2z  3556  prel12  3805  uniss  3864  ssuni  3865  intss  3899  intssuni  3900  iunss1  3932  iinss1  3933  ss2iun  3936  disjss2  4012  disjss1  4015  disjss3  4038  ssbrd  4080  sspwb  4239  poss  4332  pofun  4346  soss  4348  frss  4376  sess1  4377  sess2  4378  wess  4396  trsuc2OLD  4493  reusv6OLD  4561  dfwe2  4589  onint  4602  orduniorsuc  4637  ordom  4681  finds  4698  finds2  4700  relss  4791  ssrel  4792  ssrelrel  4803  xpsspw  4813  relop  4850  cnvss  4870  dmss  4894  dmcosseq  4962  funss  5289  fss  5413  fun  5421  brprcneu  5534  f1eqcocnv  5821  isores3  5848  isomin  5850  isopolem  5858  isosolem  5860  isowe2  5863  f1oweALT  5867  tposfn2  6272  tposfo2  6273  tposf1o2  6276  smores  6385  tz7.48lem  6469  tz7.48-3  6472  oaass  6575  iiner  6747  xpdom2  6973  ssenen  7051  pssnn  7097  hartogs  7275  card2on  7284  ackbij1  7880  cfub  7891  fin23lem27  7970  fin1a2lem11  8052  fin1a2lem13  8054  hsmexlem2  8069  ondomon  8201  gchina  8337  intgru  8452  ingru  8453  addclprlem2  8657  psslinpr  8671  ltexprlem3  8678  ltexprlem4  8679  reclem2pr  8688  suplem1pr  8692  sup2  9726  nnind  9780  nnunb  9977  uzind  10119  xmullem2  10601  xrsupsslem  10641  xrinfmsslem  10642  seqof  11119  hashfacen  11408  sswrd  11439  wrdind  11493  cau3lem  11854  caubnd  11858  vdwnnlem2  13059  ramub2  13077  fthres2  13822  odupos  14255  lsmdisj2  15007  pgpfac1lem3  15328  subrgdvds  15575  lspdisj  15894  lspprat  15922  lbsextlem2  15928  ocv2ss  16589  ocvin  16590  tgcl  16723  epttop  16762  cmpsub  17143  tgcmp  17144  hauscmplem  17149  dfcon2  17161  llyss  17221  nllyss  17222  txcnpi  17318  txcnp  17330  snfil  17575  fgcl  17589  filcon  17594  filuni  17596  cfinfil  17604  csdfil  17605  supfil  17606  ufildom1  17637  fin1aufil  17643  fmfnfmlem3  17667  ptcmplem2  17763  cldsubg  17809  iscau3  18720  iscau4  18721  caussi  18739  volfiniun  18920  plycj  19674  abelth  19833  wilthlem2  20323  lgsdir2lem4  20581  pntleml  20776  lpni  20862  ubthlem1  21465  chintcli  21926  h1de2i  22148  spansnm0i  22245  strlem1  22846  mdslmd1i  22925  2reuswap2  23153  ssrmo  23164  disjss1f  23366  disjpreima  23376  sigaclfu2  23497  derangenlem  23717  conpcon  23781  cvmsss2  23820  sltres  24389  nocvxmin  24416  naim1  24895  naim2  24896  waj-ax  24925  lukshef-ax2  24926  itg2addnclem  25003  itg2addnc  25005  diaimd  25113  inttop2  25618  qusp  25645  dualded  25886  dualcat2  25887  locfincmp  26407  ismtybndlem  26633  ablo4pnp  26673  isdrngo3  26693  keridl  26760  ispridl2  26766  ispridlc  26798  prter1  26850  mzpindd  26927  pellexlem3  27019  pellexlem5  27021  pellex  27023  2nn0ind  27133  lnr2i  27423  pm10.56  27668  ssrexf  27787  stoweidlem61  27913  2rmoswap  28065  ax12-3  29726  a12stdy1-x12  29733  a12stdy1  29748  a12studyALT  29755  lshpdisj  29799  snatpsubN  30561  pmapglb2N  30582  pmapglb2xN  30583  elpaddn0  30611
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 177
  Copyright terms: Public domain W3C validator