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  1296  3orim123d  1297  mo3  2298  mo3OLD  2299  moim  2319  morimvOLD  2322  2euswap  2357  ralim  2792  ralimdaa  2798  ralimdv2  2801  rexim  2825  reximdv2  2830  moeq3  3141  rmoim  3163  2reuswap  3166  ssel  3355  sstr2  3368  sscon  3495  ssdif  3496  unss1  3530  ssrin  3580  difin0ss  3750  r19.2z  3774  prel12  4054  uniss  4117  ssuni  4118  intss  4154  intssuni  4155  iunss1  4187  iinss1  4188  ss2iun  4191  disjss2  4270  disjss1  4273  disjss3  4296  ssbrd  4338  reusv6OLD  4508  sspwb  4546  poss  4648  pofun  4662  soss  4664  frss  4692  sess1  4693  sess2  4694  wess  4712  relss  4932  ssrel  4933  ssrel2  4935  ssrelrel  4945  xpsspw  4958  relop  4995  cnvss  5017  dmss  5044  dmcosseq  5106  funss  5441  fss  5572  fun  5580  brprcneu  5689  f1eqcocnv  6004  isores3  6031  isomin  6033  isopolem  6041  isosolem  6043  isowe2  6046  ovmpt2s  6219  dfwe2  6398  onint  6411  orduniorsuc  6446  ordom  6490  finds  6507  finds2  6509  f1oweALT  6566  tposfn2  6772  tposfo2  6773  tposf1o2  6776  smores  6818  tz7.48lem  6901  tz7.48-3  6904  oaass  7005  iiner  7177  xpdom2  7411  ssenen  7490  pssnn  7536  hartogs  7763  card2on  7774  ackbij1  8412  cfub  8423  fin23lem27  8502  fin1a2lem11  8584  fin1a2lem13  8586  hsmexlem2  8601  zorn2lem4  8673  ondomon  8732  gchina  8871  intgru  8986  ingru  8987  addclprlem2  9191  psslinpr  9205  ltexprlem3  9212  ltexprlem4  9213  reclem2pr  9222  suplem1pr  9226  sup2  10291  nnind  10345  nnunb  10580  uzind  10738  xmullem2  11233  xrsupsslem  11274  xrinfmsslem  11275  seqof  11868  hashfacen  12212  sswrd  12247  wrdind  12376  wrd2ind  12377  swrdccatin12lem2  12385  cau3lem  12847  caubnd  12851  vdwnnlem2  14062  ramub2  14080  fthres2  14847  odupos  15310  lsmdisj2  16184  pgpfac1lem3  16583  subrgdvds  16884  lspdisj  17211  lspprat  17239  lbsextlem2  17245  evl1gsumd  17796  ocv2ss  18103  ocvin  18104  tgcl  18579  epttop  18618  cmpsub  19008  tgcmp  19009  hauscmplem  19014  dfcon2  19028  llyss  19088  nllyss  19089  txcnpi  19186  txcnp  19198  snfil  19442  fgcl  19456  filcon  19461  filuni  19463  cfinfil  19471  csdfil  19472  supfil  19473  ufildom1  19504  fin1aufil  19510  fmfnfmlem3  19534  ptcmplem2  19630  cldsubg  19686  iscau3  20794  iscau4  20795  caussi  20813  volfiniun  21033  plycj  21749  abelth  21911  wilthlem2  22412  lgsdir2lem4  22670  pntleml  22865  cusgrafilem2  23393  lpni  23671  ubthlem1  24276  chintcli  24739  h1de2i  24961  spansnm0i  25058  strlem1  25659  mdslmd1i  25738  2reuswap2  25877  ssrmo  25883  rabss3d  25900  disjss1f  25923  disjpreima  25933  ssrelf  25950  nnindf  26094  esumpcvgval  26532  derangenlem  27064  conpcon  27129  cvmsss2  27168  pocnv  27579  wzel  27766  sltres  27810  nocvxmin  27837  naim1  28236  naim2  28237  waj-ax  28265  lukshef-ax2  28266  itg2addnclem  28448  locfincmp  28581  ismtybndlem  28710  ablo4pnp  28750  isdrngo3  28770  keridl  28837  ispridl2  28843  ispridlc  28875  prter1  29029  mzpindd  29087  pellexlem3  29177  pellexlem5  29179  pellex  29181  2nn0ind  29291  lnr2i  29477  ssrexf  29740  2rmoswap  30013  frisusgranb  30594  frgrancvvdeqlem3  30630  coe1fzgsumd  30843  lshpdisj  32637  snatpsubN  33399  pmapglb2N  33420  pmapglb2xN  33421  elpaddn0  33449
  Copyright terms: Public domain W3C validator