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  2308  moim  2320  2euswap  2349  nelcon3d  2708  ral2imi  2748  ralimOLD  2754  ralimdaaOLD  2763  ralimdv2  2767  rexim  2824  reximd2a  2829  reximdv2  2830  moeq3  3185  rmoim  3209  2reuswap  3212  ssel  3396  sstr2  3409  ssrexf  3462  sscon  3537  ssdif  3538  unss1  3573  ssrin  3625  difin0ss  3801  r19.2z  3826  prel12  4115  uniss  4178  ssuni  4179  intssOLD  4215  intssuni  4216  iunss1  4249  iinss1  4250  ss2iun  4253  disjss2  4335  disjss1  4338  disjss3  4360  ssbrd  4403  sspwb  4608  poss  4714  pofun  4728  soss  4730  frss  4758  sess1  4759  sess2  4760  wess  4778  relss  4879  ssrel  4880  ssrel2  4882  ssrelrel  4892  relop  4942  cnvss  4964  dmss  4991  dmcosseq  5053  funss  5557  fss  5692  fun  5701  brprcneu  5813  f1eqcocnv  6153  isores3  6180  isomin  6182  isopolem  6190  isosolem  6192  isowe2  6195  ovmpt2s  6373  dfwe2  6561  onint  6575  orduniorsuc  6610  ordom  6654  finds  6672  finds2  6674  f1oweALT  6730  tposfn2  6945  tposfo2  6946  tposf1o2  6949  smores  7021  tz7.48lem  7108  tz7.48-3  7111  oaass  7212  iiner  7385  xpdom2  7615  ssenen  7694  pssnn  7738  hartogs  8007  card2on  8017  ackbij1  8614  cfub  8625  fin23lem27  8704  fin1a2lem11  8786  fin1a2lem13  8788  hsmexlem2  8803  zorn2lem4  8875  ondomon  8934  gchina  9070  intgru  9185  ingru  9186  addclprlem2  9388  psslinpr  9402  ltexprlem3  9409  ltexprlem4  9410  reclem2pr  9419  suplem1pr  9423  sup2  10511  nnind  10573  nnunb  10811  uzind  10973  xmullem2  11497  xrsupsslem  11538  xrinfmsslem  11539  seqof  12215  hashfacen  12560  sswrd  12622  sswrdOLD  12623  wrdind  12774  wrd2ind  12775  swrdccatin12lem2  12786  cau3lem  13356  caubnd  13360  vdwnnlem2  14884  ramub2  14909  fthres2  15775  odupos  16319  lsmdisj2  17270  pgpfac1lem3  17648  subrgdvds  17960  lspdisj  18286  lspprat  18314  lbsextlem2  18320  coe1fzgsumd  18834  evl1gsumd  18883  ocv2ss  19173  ocvin  19174  tgcl  19922  epttop  19961  cmpsub  20352  tgcmp  20353  hauscmplem  20358  dfcon2  20371  llyss  20431  nllyss  20432  locfincmp  20478  txcnpi  20560  txcnp  20572  snfil  20816  fgcl  20830  filcon  20835  filuni  20837  cfinfil  20845  csdfil  20846  supfil  20847  ufildom1  20878  fin1aufil  20884  fmfnfmlem3  20908  ptcmplem2  21005  cldsubg  21062  iscau3  22185  iscau4  22186  caussi  22204  volfiniun  22437  plycj  23168  abelth  23333  wilthlem2  23931  lgsdir2lem4  24191  pntleml  24386  cusgrafilem2  25145  frisusgranb  25662  frgrancvvdeqlem3  25697  lpni  25848  ubthlem1  26449  chintcli  26921  h1de2i  27143  spansnm0i  27240  strlem1  27840  mdslmd1i  27919  2reuswap2  28061  ssrmo  28067  rabss3d  28086  iunxdif3  28116  disjss1f  28124  disjpreima  28135  ssrelf  28162  suppss3  28257  nnindf  28328  oduprs  28363  crefss  28623  esumpcvgval  28846  derangenlem  29841  conpcon  29905  cvmsss2  29944  pocnv  30350  wzel  30453  sltres  30497  nocvxmin  30524  naim1  30989  naim2  30990  waj-ax  31018  lukshef-ax2  31019  bj-mo3OLD  31358  poimirlem26  31873  poimirlem30  31877  poimirlem32  31879  itg2addnclem  31900  ismtybndlem  32045  ablo4pnp  32085  isdrngo3  32105  keridl  32172  ispridl2  32178  ispridlc  32210  prter1  32362  lshpdisj  32465  snatpsubN  33227  pmapglb2N  33248  pmapglb2xN  33249  elpaddn0  33277  mzpindd  35500  pellexlem3  35588  pellexlem5  35590  pellex  35592  2nn0ind  35706  lnr2i  35888  intabssd  36129  iunrelexpuztr  36224  hess  36288  frege52aid  36367  frege52b  36398  2rmoswap  38419  pfxccatin12lem2  38778  uhgr0vsize0  39060  cusgrfilem2  39245  nrhmzr  39464
  Copyright terms: Public domain W3C validator