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  1304  3orim123d  1305  mo3  2268  mo3OLD  2269  moim  2281  2euswap  2311  nelcon3d  2741  ral2imi  2780  ralimOLD  2786  ralimdaaOLD  2795  ralimdv2  2799  rexim  2857  reximd2a  2862  reximdv2  2863  moeq3  3214  rmoim  3237  2reuswap  3240  ssel  3424  sstr2  3437  ssrexf  3490  sscon  3565  ssdif  3566  unss1  3600  ssrin  3650  difin0ss  3823  r19.2z  3847  prel12  4134  uniss  4197  ssuni  4198  intssOLD  4234  intssuni  4235  iunss1  4268  iinss1  4269  ss2iun  4272  disjss2  4354  disjss1  4357  disjss3  4379  ssbrd  4421  sspwb  4624  poss  4729  pofun  4743  soss  4745  frss  4773  sess1  4774  sess2  4775  wess  4793  relss  5016  ssrel  5017  ssrel2  5019  ssrelrel  5029  relop  5079  cnvss  5101  dmss  5128  dmcosseq  5190  funss  5527  fss  5660  fun  5669  brprcneu  5780  f1eqcocnv  6123  isores3  6150  isomin  6152  isopolem  6160  isosolem  6162  isowe2  6165  ovmpt2s  6343  dfwe2  6534  onint  6547  orduniorsuc  6582  ordom  6626  finds  6643  finds2  6645  f1oweALT  6701  tposfn2  6913  tposfo2  6914  tposf1o2  6917  smores  6959  tz7.48lem  7042  tz7.48-3  7045  oaass  7146  iiner  7319  xpdom2  7549  ssenen  7628  pssnn  7672  hartogs  7902  card2on  7913  ackbij1  8549  cfub  8560  fin23lem27  8639  fin1a2lem11  8721  fin1a2lem13  8723  hsmexlem2  8738  zorn2lem4  8810  ondomon  8869  gchina  9006  intgru  9121  ingru  9122  addclprlem2  9324  psslinpr  9338  ltexprlem3  9345  ltexprlem4  9346  reclem2pr  9355  suplem1pr  9359  sup2  10433  nnind  10488  nnunb  10726  uzind  10889  xmullem2  11396  xrsupsslem  11437  xrinfmsslem  11438  seqof  12086  hashfacen  12426  sswrd  12480  sswrdOLD  12481  wrdind  12632  wrd2ind  12633  swrdccatin12lem2  12644  cau3lem  13208  caubnd  13212  vdwnnlem2  14535  ramub2  14553  fthres2  15357  odupos  15901  lsmdisj2  16836  pgpfac1lem3  17260  subrgdvds  17575  lspdisj  17903  lspprat  17931  lbsextlem2  17937  coe1fzgsumd  18476  evl1gsumd  18525  ocv2ss  18814  ocvin  18815  tgcl  19575  epttop  19614  cmpsub  20005  tgcmp  20006  hauscmplem  20011  dfcon2  20024  llyss  20084  nllyss  20085  locfincmp  20131  txcnpi  20213  txcnp  20225  snfil  20469  fgcl  20483  filcon  20488  filuni  20490  cfinfil  20498  csdfil  20499  supfil  20500  ufildom1  20531  fin1aufil  20537  fmfnfmlem3  20561  ptcmplem2  20657  cldsubg  20713  iscau3  21821  iscau4  21822  caussi  21840  volfiniun  22061  plycj  22778  abelth  22940  wilthlem2  23479  lgsdir2lem4  23737  pntleml  23932  cusgrafilem2  24622  frisusgranb  25139  frgrancvvdeqlem3  25174  lpni  25323  ubthlem1  25924  chintcli  26387  h1de2i  26609  spansnm0i  26706  strlem1  27306  mdslmd1i  27385  2reuswap2  27527  ssrmo  27533  rabss3d  27553  iunxdif3  27584  disjss1f  27592  disjpreima  27603  ssrelf  27630  suppss3  27730  nnindf  27793  oduprs  27827  crefss  28037  esumpcvgval  28257  derangenlem  28840  conpcon  28905  cvmsss2  28944  pocnv  29395  wzel  29581  sltres  29625  nocvxmin  29652  naim1  30039  naim2  30040  waj-ax  30068  lukshef-ax2  30069  itg2addnclem  30268  ismtybndlem  30504  ablo4pnp  30544  isdrngo3  30564  keridl  30631  ispridl2  30637  ispridlc  30669  prter1  30822  mzpindd  30880  pellexlem3  30968  pellexlem5  30970  pellex  30972  2nn0ind  31082  lnr2i  31269  2rmoswap  32390  pfxccatin12lem2  32634  nrhmzr  32914  lshpdisj  35160  snatpsubN  35922  pmapglb2N  35943  pmapglb2xN  35944  elpaddn0  35972  iunrelexpuztr  38259  hess  38309  frege52aid  38392  frege52b  38423
  Copyright terms: Public domain W3C validator