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

Theorem 3imtr4g 273
Description: More general version of 3imtr4i 269. 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 220 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 230 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3anim123d  1342  3orim123d  1343  mo3  2306  moim  2318  2euswap  2348  nelcon3d  2781  ral2imi  2820  ralimOLD  2826  ralimdaaOLD  2835  ralimdv2  2839  rexim  2897  reximd2a  2902  reximdv2  2903  moeq3  3254  rmoim  3277  2reuswap  3280  ssel  3464  sstr2  3477  ssrexf  3530  sscon  3605  ssdif  3606  unss1  3641  ssrin  3693  difin0ss  3867  r19.2z  3892  prel12  4180  uniss  4243  ssuni  4244  intssOLD  4280  intssuni  4281  iunss1  4314  iinss1  4315  ss2iun  4318  disjss2  4400  disjss1  4403  disjss3  4425  ssbrd  4467  sspwb  4671  poss  4777  pofun  4791  soss  4793  frss  4821  sess1  4822  sess2  4823  wess  4841  relss  4942  ssrel  4943  ssrel2  4945  ssrelrel  4955  relop  5005  cnvss  5027  dmss  5054  dmcosseq  5116  funss  5619  fss  5754  fun  5763  brprcneu  5874  f1eqcocnv  6214  isores3  6241  isomin  6243  isopolem  6251  isosolem  6253  isowe2  6256  ovmpt2s  6434  dfwe2  6622  onint  6636  orduniorsuc  6671  ordom  6715  finds  6733  finds2  6735  f1oweALT  6791  tposfn2  7003  tposfo2  7004  tposf1o2  7007  smores  7079  tz7.48lem  7166  tz7.48-3  7169  oaass  7270  iiner  7443  xpdom2  7673  ssenen  7752  pssnn  7796  hartogs  8059  card2on  8069  ackbij1  8666  cfub  8677  fin23lem27  8756  fin1a2lem11  8838  fin1a2lem13  8840  hsmexlem2  8855  zorn2lem4  8927  ondomon  8986  gchina  9123  intgru  9238  ingru  9239  addclprlem2  9441  psslinpr  9455  ltexprlem3  9462  ltexprlem4  9463  reclem2pr  9472  suplem1pr  9476  sup2  10565  nnind  10627  nnunb  10865  uzind  11027  xmullem2  11551  xrsupsslem  11592  xrinfmsslem  11593  seqof  12267  hashfacen  12612  sswrd  12666  sswrdOLD  12667  wrdind  12818  wrd2ind  12819  swrdccatin12lem2  12830  cau3lem  13396  caubnd  13400  vdwnnlem2  14909  ramub2  14934  fthres2  15788  odupos  16332  lsmdisj2  17267  pgpfac1lem3  17645  subrgdvds  17957  lspdisj  18283  lspprat  18311  lbsextlem2  18317  coe1fzgsumd  18831  evl1gsumd  18880  ocv2ss  19167  ocvin  19168  tgcl  19916  epttop  19955  cmpsub  20346  tgcmp  20347  hauscmplem  20352  dfcon2  20365  llyss  20425  nllyss  20426  locfincmp  20472  txcnpi  20554  txcnp  20566  snfil  20810  fgcl  20824  filcon  20829  filuni  20831  cfinfil  20839  csdfil  20840  supfil  20841  ufildom1  20872  fin1aufil  20878  fmfnfmlem3  20902  ptcmplem2  20999  cldsubg  21056  iscau3  22141  iscau4  22142  caussi  22160  volfiniun  22377  plycj  23099  abelth  23261  wilthlem2  23859  lgsdir2lem4  24117  pntleml  24312  cusgrafilem2  25053  frisusgranb  25570  frgrancvvdeqlem3  25605  lpni  25756  ubthlem1  26357  chintcli  26819  h1de2i  27041  spansnm0i  27138  strlem1  27738  mdslmd1i  27817  2reuswap2  27959  ssrmo  27965  rabss3d  27984  iunxdif3  28014  disjss1f  28022  disjpreima  28033  ssrelf  28060  suppss3  28155  nnindf  28220  oduprs  28255  crefss  28515  esumpcvgval  28738  derangenlem  29682  conpcon  29746  cvmsss2  29785  pocnv  30191  wzel  30294  sltres  30338  nocvxmin  30365  naim1  30830  naim2  30831  waj-ax  30859  lukshef-ax2  30860  bj-mo3OLD  31198  poimirlem26  31670  poimirlem30  31674  poimirlem32  31676  itg2addnclem  31697  ismtybndlem  31842  ablo4pnp  31882  isdrngo3  31902  keridl  31969  ispridl2  31975  ispridlc  32007  prter1  32159  lshpdisj  32262  snatpsubN  33024  pmapglb2N  33045  pmapglb2xN  33046  elpaddn0  33074  mzpindd  35297  pellexlem3  35385  pellexlem5  35387  pellex  35389  2nn0ind  35499  lnr2i  35681  iunrelexpuztr  35950  hess  36012  frege52aid  36091  frege52b  36122  2rmoswap  37996  pfxccatin12lem2  38355  nrhmzr  38631
  Copyright terms: Public domain W3C validator