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  1305  3orim123d  1306  mo3  2307  mo3OLD  2308  moim  2323  morimvOLD  2326  2euswap  2354  nelcon3d  2790  ral2imi  2829  ralimOLD  2835  ralimdaaOLD  2844  ralimdv2  2848  rexim  2906  reximd2a  2911  reximdv2  2912  moeq3  3260  rmoim  3283  2reuswap  3286  ssel  3480  sstr2  3493  sscon  3620  ssdif  3621  unss1  3655  ssrin  3705  difin0ss  3876  r19.2z  3900  prel12  4188  uniss  4251  ssuni  4252  intssOLD  4288  intssuni  4290  iunss1  4323  iinss1  4324  ss2iun  4327  disjss2  4406  disjss1  4409  disjss3  4432  ssbrd  4474  reusv6OLD  4644  sspwb  4682  poss  4788  pofun  4802  soss  4804  frss  4832  sess1  4833  sess2  4834  wess  4852  relss  5076  ssrel  5077  ssrel2  5079  ssrelrel  5089  xpsspw  5102  relop  5139  cnvss  5161  dmss  5188  dmcosseq  5250  funss  5592  fss  5725  fun  5734  brprcneu  5845  f1eqcocnv  6185  isores3  6212  isomin  6214  isopolem  6222  isosolem  6224  isowe2  6227  ovmpt2s  6407  dfwe2  6598  onint  6611  orduniorsuc  6646  ordom  6690  finds  6707  finds2  6709  f1oweALT  6765  tposfn2  6975  tposfo2  6976  tposf1o2  6979  smores  7021  tz7.48lem  7104  tz7.48-3  7107  oaass  7208  iiner  7381  xpdom2  7610  ssenen  7689  pssnn  7736  hartogs  7967  card2on  7978  ackbij1  8616  cfub  8627  fin23lem27  8706  fin1a2lem11  8788  fin1a2lem13  8790  hsmexlem2  8805  zorn2lem4  8877  ondomon  8936  gchina  9075  intgru  9190  ingru  9191  addclprlem2  9393  psslinpr  9407  ltexprlem3  9414  ltexprlem4  9415  reclem2pr  9424  suplem1pr  9428  sup2  10500  nnind  10555  nnunb  10792  uzind  10955  xmullem2  11461  xrsupsslem  11502  xrinfmsslem  11503  seqof  12138  hashfacen  12477  sswrd  12529  wrdind  12676  wrd2ind  12677  swrdccatin12lem2  12688  cau3lem  13161  caubnd  13165  vdwnnlem2  14386  ramub2  14404  fthres2  15170  odupos  15634  lsmdisj2  16569  pgpfac1lem3  16996  subrgdvds  17311  lspdisj  17639  lspprat  17667  lbsextlem2  17673  coe1fzgsumd  18212  evl1gsumd  18261  ocv2ss  18571  ocvin  18572  tgcl  19337  epttop  19376  cmpsub  19766  tgcmp  19767  hauscmplem  19772  dfcon2  19786  llyss  19846  nllyss  19847  locfincmp  19893  txcnpi  19975  txcnp  19987  snfil  20231  fgcl  20245  filcon  20250  filuni  20252  cfinfil  20260  csdfil  20261  supfil  20262  ufildom1  20293  fin1aufil  20299  fmfnfmlem3  20323  ptcmplem2  20419  cldsubg  20475  iscau3  21583  iscau4  21584  caussi  21602  volfiniun  21823  plycj  22539  abelth  22701  wilthlem2  23208  lgsdir2lem4  23466  pntleml  23661  cusgrafilem2  24345  frisusgranb  24862  frgrancvvdeqlem3  24897  lpni  25046  ubthlem1  25651  chintcli  26114  h1de2i  26336  spansnm0i  26433  strlem1  27034  mdslmd1i  27113  2reuswap2  27252  ssrmo  27258  rabss3d  27277  disjss1f  27300  disjpreima  27310  ssrelf  27331  suppss3  27415  nnindf  27476  oduprs  27510  crefss  27718  esumpcvgval  27950  derangenlem  28481  conpcon  28546  cvmsss2  28585  pocnv  29161  wzel  29348  sltres  29392  nocvxmin  29419  naim1  29818  naim2  29819  waj-ax  29847  lukshef-ax2  29848  itg2addnclem  30034  ismtybndlem  30270  ablo4pnp  30310  isdrngo3  30330  keridl  30397  ispridl2  30403  ispridlc  30435  prter1  30588  mzpindd  30646  pellexlem3  30735  pellexlem5  30737  pellex  30739  2nn0ind  30849  lnr2i  31033  ssrexf  31335  2rmoswap  32023  lshpdisj  34414  snatpsubN  35176  pmapglb2N  35197  pmapglb2xN  35198  elpaddn0  35226  bj-frege52a  37516
  Copyright terms: Public domain W3C validator