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

Theorem 3imtr4g 278
Description: More general version of 3imtr4i 274. 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 225 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 235 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3anim123d  1355  3orim123d  1356  mo3  2347  moim  2359  2euswap  2388  nelcon3d  2748  ral2imi  2788  ralimOLD  2794  ralimdaaOLD  2803  ralimdv2  2807  rexim  2864  reximd2a  2869  reximdv2  2870  moeq3  3227  rmoim  3251  2reuswap  3254  ssel  3438  sstr2  3451  ssrexf  3504  sscon  3579  ssdif  3580  unss1  3615  ssrin  3669  difin0ss  3845  r19.2z  3870  prel12  4165  uniss  4233  ssuni  4234  intssOLD  4270  intssuni  4271  iunss1  4304  iinss1  4305  ss2iun  4308  disjss2  4390  disjss1  4393  disjss3  4415  ssbrd  4458  sspwb  4663  poss  4776  pofun  4790  soss  4792  frss  4820  sess1  4821  sess2  4822  wess  4840  relss  4941  ssrel  4942  ssrel2  4944  ssrelrel  4954  relop  5004  cnvss  5026  dmss  5053  dmcosseq  5115  funss  5619  fss  5760  fun  5769  brprcneu  5881  f1eqcocnv  6224  isores3  6251  isomin  6253  isopolem  6261  isosolem  6263  isowe2  6266  ovmpt2s  6447  dfwe2  6635  onint  6649  orduniorsuc  6684  ordom  6728  finds  6746  finds2  6748  f1oweALT  6804  tposfn2  7021  tposfo2  7022  tposf1o2  7025  smores  7097  tz7.48lem  7184  tz7.48-3  7187  oaass  7288  iiner  7461  xpdom2  7693  ssenen  7772  pssnn  7816  hartogs  8085  card2on  8095  ackbij1  8694  cfub  8705  fin23lem27  8784  fin1a2lem11  8866  fin1a2lem13  8868  hsmexlem2  8883  zorn2lem4  8955  ondomon  9014  gchina  9150  intgru  9265  ingru  9266  addclprlem2  9468  psslinpr  9482  ltexprlem3  9489  ltexprlem4  9490  reclem2pr  9499  suplem1pr  9503  sup2  10593  nnind  10655  nnunb  10894  uzind  11056  xmullem2  11580  xrsupsslem  11621  xrinfmsslem  11622  seqof  12302  hashfacen  12650  sswrd  12712  sswrdOLD  12713  wrdind  12870  wrd2ind  12871  swrdccatin12lem2  12882  cau3lem  13466  caubnd  13470  vdwnnlem2  14995  ramub2  15020  fthres2  15886  odupos  16430  lsmdisj2  17381  pgpfac1lem3  17759  subrgdvds  18071  lspdisj  18397  lspprat  18425  lbsextlem2  18431  coe1fzgsumd  18945  evl1gsumd  18994  ocv2ss  19285  ocvin  19286  tgcl  20034  epttop  20073  cmpsub  20464  tgcmp  20465  hauscmplem  20470  dfcon2  20483  llyss  20543  nllyss  20544  locfincmp  20590  txcnpi  20672  txcnp  20684  snfil  20928  fgcl  20942  filcon  20947  filuni  20949  cfinfil  20957  csdfil  20958  supfil  20959  ufildom1  20990  fin1aufil  20996  fmfnfmlem3  21020  ptcmplem2  21117  cldsubg  21174  iscau3  22297  iscau4  22298  caussi  22316  volfiniun  22549  plycj  23280  abelth  23445  wilthlem2  24043  lgsdir2lem4  24303  pntleml  24498  cusgrafilem2  25257  frisusgranb  25774  frgrancvvdeqlem3  25809  lpni  25960  ubthlem1  26561  chintcli  27033  h1de2i  27255  spansnm0i  27352  strlem1  27952  mdslmd1i  28031  2reuswap2  28173  ssrmo  28179  rabss3d  28197  iunxdif3  28224  disjss1f  28232  disjpreima  28243  ssrelf  28270  suppss3  28361  nnindf  28431  oduprs  28466  crefss  28725  esumpcvgval  28948  derangenlem  29943  conpcon  30007  cvmsss2  30046  pocnv  30453  wzel  30556  sltres  30600  nocvxmin  30629  naim1  31094  naim2  31095  waj-ax  31123  lukshef-ax2  31124  bj-ssbim  31279  bj-mo3OLD  31492  poimirlem26  32011  poimirlem30  32015  poimirlem32  32017  itg2addnclem  32038  ismtybndlem  32183  ablo4pnp  32223  isdrngo3  32243  keridl  32310  ispridl2  32316  ispridlc  32348  prter1  32496  lshpdisj  32598  snatpsubN  33360  pmapglb2N  33381  pmapglb2xN  33382  elpaddn0  33410  mzpindd  35633  pellexlem3  35720  pellexlem5  35722  pellex  35724  2nn0ind  35838  lnr2i  36020  intabssd  36261  iunrelexpuztr  36356  hess  36420  frege52aid  36499  frege52b  36530  2rmoswap  38643  pfxccatin12lem2  39005  uhgr0vsize0  39365  cusgrfilem2  39567  uhgrvd00  39621  nrhmzr  40146
  Copyright terms: Public domain W3C validator