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

Theorem 3imtr4g 262
Description: More general version of 3imtr4i 258. 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 209 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 219 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3anim123d  1261  3orim123d  1262  moim  2300  morimv  2302  2euswap  2330  ralim  2737  ralimdaa  2743  ralimdv2  2746  rexim  2770  reximdv2  2775  moeq3  3071  rmoim  3093  2reuswap  3096  ssel  3302  sstr2  3315  sscon  3441  ssdif  3442  unss1  3476  ssrin  3526  difin0ss  3654  r19.2z  3677  prel12  3935  uniss  3996  ssuni  3997  intss  4031  intssuni  4032  iunss1  4064  iinss1  4065  ss2iun  4068  disjss2  4145  disjss1  4148  disjss3  4171  ssbrd  4213  sspwb  4373  poss  4465  pofun  4479  soss  4481  frss  4509  sess1  4510  sess2  4511  wess  4529  reusv6OLD  4693  dfwe2  4721  onint  4734  orduniorsuc  4769  ordom  4813  finds  4830  finds2  4832  relss  4922  ssrel  4923  ssrel2  4925  ssrelrel  4935  xpsspw  4945  relop  4982  cnvss  5004  dmss  5028  dmcosseq  5096  funss  5431  fss  5558  fun  5566  brprcneu  5680  f1eqcocnv  5987  isores3  6014  isomin  6016  isopolem  6024  isosolem  6026  isowe2  6029  f1oweALT  6033  tposfn2  6460  tposfo2  6461  tposf1o2  6464  smores  6573  tz7.48lem  6657  tz7.48-3  6660  oaass  6763  iiner  6935  xpdom2  7162  ssenen  7240  pssnn  7286  hartogs  7469  card2on  7478  ackbij1  8074  cfub  8085  fin23lem27  8164  fin1a2lem11  8246  fin1a2lem13  8248  hsmexlem2  8263  zorn2lem4  8335  ondomon  8394  gchina  8530  intgru  8645  ingru  8646  addclprlem2  8850  psslinpr  8864  ltexprlem3  8871  ltexprlem4  8872  reclem2pr  8881  suplem1pr  8885  sup2  9920  nnind  9974  nnunb  10173  uzind  10317  xmullem2  10800  xrsupsslem  10841  xrinfmsslem  10842  seqof  11335  hashfacen  11658  sswrd  11692  wrdind  11746  cau3lem  12113  caubnd  12117  vdwnnlem2  13319  ramub2  13337  fthres2  14084  odupos  14517  lsmdisj2  15269  pgpfac1lem3  15590  subrgdvds  15837  lspdisj  16152  lspprat  16180  lbsextlem2  16186  ocv2ss  16855  ocvin  16856  tgcl  16989  epttop  17028  cmpsub  17417  tgcmp  17418  hauscmplem  17423  dfcon2  17435  llyss  17495  nllyss  17496  txcnpi  17593  txcnp  17605  snfil  17849  fgcl  17863  filcon  17868  filuni  17870  cfinfil  17878  csdfil  17879  supfil  17880  ufildom1  17911  fin1aufil  17917  fmfnfmlem3  17941  ptcmplem2  18037  cldsubg  18093  iscau3  19184  iscau4  19185  caussi  19203  volfiniun  19394  plycj  20148  abelth  20310  wilthlem2  20805  lgsdir2lem4  21063  pntleml  21258  cusgrafilem2  21442  lpni  21720  ubthlem1  22325  chintcli  22786  h1de2i  23008  spansnm0i  23105  strlem1  23706  mdslmd1i  23785  2reuswap2  23928  ssrmo  23934  rabss3d  23948  disjss1f  23969  disjpreima  23979  esumpcvgval  24421  derangenlem  24810  conpcon  24875  cvmsss2  24914  sltres  25532  nocvxmin  25559  naim1  26038  naim2  26039  waj-ax  26068  lukshef-ax2  26069  itg2addnclem  26155  locfincmp  26274  ismtybndlem  26405  ablo4pnp  26445  isdrngo3  26465  keridl  26532  ispridl2  26538  ispridlc  26570  prter1  26618  mzpindd  26693  pellexlem3  26784  pellexlem5  26786  pellex  26788  2nn0ind  26898  lnr2i  27188  pm10.56  27433  ssrexf  27551  2rmoswap  27829  swrdccatin12lem3  28024  frisusgranb  28101  frgrancvvdeqlem3  28135  lshpdisj  29470  snatpsubN  30232  pmapglb2N  30253  pmapglb2xN  30254  elpaddn0  30282
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