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

Theorem 3imtr4g 270
Description: More general version of 3imtr4i 266. 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 217 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 227 1  |-  ( ph  ->  ( th  ->  ta ) )
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:  3anim123d  1291  3orim123d  1292  mo3  2301  mo3OLD  2302  moim  2322  morimvOLD  2325  2euswap  2360  ralim  2785  ralimdaa  2791  ralimdv2  2794  rexim  2818  reximdv2  2823  moeq3  3133  rmoim  3155  2reuswap  3158  ssel  3347  sstr2  3360  sscon  3487  ssdif  3488  unss1  3522  ssrin  3572  difin0ss  3742  r19.2z  3766  prel12  4046  uniss  4109  ssuni  4110  intss  4146  intssuni  4147  iunss1  4179  iinss1  4180  ss2iun  4183  disjss2  4262  disjss1  4265  disjss3  4288  ssbrd  4330  reusv6OLD  4500  sspwb  4538  poss  4639  pofun  4653  soss  4655  frss  4683  sess1  4684  sess2  4685  wess  4703  relss  4923  ssrel  4924  ssrel2  4926  ssrelrel  4936  xpsspw  4949  relop  4986  cnvss  5008  dmss  5035  dmcosseq  5097  funss  5433  fss  5564  fun  5572  brprcneu  5681  f1eqcocnv  5996  isores3  6023  isomin  6025  isopolem  6033  isosolem  6035  isowe2  6038  ovmpt2s  6213  dfwe2  6392  onint  6405  orduniorsuc  6440  ordom  6484  finds  6501  finds2  6503  f1oweALT  6560  tposfn2  6766  tposfo2  6767  tposf1o2  6770  smores  6809  tz7.48lem  6892  tz7.48-3  6895  oaass  6996  iiner  7168  xpdom2  7402  ssenen  7481  pssnn  7527  hartogs  7754  card2on  7765  ackbij1  8403  cfub  8414  fin23lem27  8493  fin1a2lem11  8575  fin1a2lem13  8577  hsmexlem2  8592  zorn2lem4  8664  ondomon  8723  gchina  8862  intgru  8977  ingru  8978  addclprlem2  9182  psslinpr  9196  ltexprlem3  9203  ltexprlem4  9204  reclem2pr  9213  suplem1pr  9217  sup2  10282  nnind  10336  nnunb  10571  uzind  10729  xmullem2  11224  xrsupsslem  11265  xrinfmsslem  11266  seqof  11859  hashfacen  12203  sswrd  12238  wrdind  12367  wrd2ind  12368  swrdccatin12lem2  12376  cau3lem  12838  caubnd  12842  vdwnnlem2  14053  ramub2  14071  fthres2  14838  odupos  15301  lsmdisj2  16172  pgpfac1lem3  16568  subrgdvds  16859  lspdisj  17184  lspprat  17212  lbsextlem2  17218  ocv2ss  18057  ocvin  18058  tgcl  18533  epttop  18572  cmpsub  18962  tgcmp  18963  hauscmplem  18968  dfcon2  18982  llyss  19042  nllyss  19043  txcnpi  19140  txcnp  19152  snfil  19396  fgcl  19410  filcon  19415  filuni  19417  cfinfil  19425  csdfil  19426  supfil  19427  ufildom1  19458  fin1aufil  19464  fmfnfmlem3  19488  ptcmplem2  19584  cldsubg  19640  iscau3  20748  iscau4  20749  caussi  20767  volfiniun  20987  plycj  21703  abelth  21865  wilthlem2  22366  lgsdir2lem4  22624  pntleml  22819  cusgrafilem2  23323  lpni  23601  ubthlem1  24206  chintcli  24669  h1de2i  24891  spansnm0i  24988  strlem1  25589  mdslmd1i  25668  2reuswap2  25807  ssrmo  25813  rabss3d  25830  disjss1f  25853  disjpreima  25863  ssrelf  25880  nnindf  26022  esumpcvgval  26463  derangenlem  26989  conpcon  27054  cvmsss2  27093  pocnv  27503  wzel  27690  sltres  27734  nocvxmin  27761  naim1  28160  naim2  28161  waj-ax  28190  lukshef-ax2  28191  itg2addnclem  28368  locfincmp  28501  ismtybndlem  28630  ablo4pnp  28670  isdrngo3  28690  keridl  28757  ispridl2  28763  ispridlc  28795  prter1  28949  mzpindd  29007  pellexlem3  29097  pellexlem5  29099  pellex  29101  2nn0ind  29211  lnr2i  29397  ssrexf  29660  2rmoswap  29933  frisusgranb  30514  frgrancvvdeqlem3  30550  lshpdisj  32354  snatpsubN  33116  pmapglb2N  33137  pmapglb2xN  33138  elpaddn0  33166
  Copyright terms: Public domain W3C validator