Theorem 3imtr4g 551

Description: More general version of 3imtr4 219. Useful for converting definitions in a formula.

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

Step	Hyp	Ref	Expression
1		3imtr4g.1	. 2 |- (ph -> (ps -> ch))
2		3imtr4g.2	. . 3 |- (th <-> ps)
3	2	bicomi 172	. 2 |- (ps <-> th)
4		3imtr4g.3	. . 3 |- (ta <-> ch)
5	4	bicomi 172	. 2 |- (ch <-> ta)
6	1, 3, 5	3imtr3g 550	1 |- (ph -> (th -> ta))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm3.48 555  pm5.74 581  ordi 594  3anim123d 897  3orim123d 898  19.22 1035  hbbid 1108  a12stdy1 1365  a12studyALT 1372  immo 1410  moimv 1412  2euswap 1438  hbabd 1461  r19.20 1694  r19.20da 1700  r19.20dv2 1703  r19.22dv2 1728  moeq3 1912  2reuswap 1927  hbcsb1g 2014  hbcsbg 2016  ssel 2053  sstr2 2061  sscon 2161  ssdif 2162  unss1 2189  ssrin 2224  difin0ss 2322  r19.2z 2337  prel12 2475  ssuni 2512  intss 2544  intssuni 2545  ss2iun 2567  iununi 2606  ssbrd 2646  sspwb 2745  poss 2832  soss 2843  frss 2911  dfwe2 2925  wess 2926  onint 2996  orduniorsuc 3077  nnsuc 3138  finds 3146  finds2 3148  relss 3236  ssxp 3246  relop 3265  cnvss 3280  dmss 3299  dffun7 3526  fun 3626  isomin 3884  f1oweALT 3891  tz7.48lem 3940  tz7.48-3 3943  oaass 4179  ss2ixp 4338  xpdom2 4422  ensdomtr 4451  domsdomtr 4456  mapenlem2 4470  mapdom2 4474  ssenen 4484  pssnn 4513  ssnn 4514  r1pwcl 4659  zorn2lem4 4763  zorn2lem7 4766  ondomon 4828  alephval3 4875  cfub 4880  1pr 5089  addclprlem2 5091  distrlem1pr 5099  psslinpr 5107  ltexprlem3 5116  ltexprlem4 5117  reclem2pr 5129  suplem1pr 5133  suppsr2 5195  suppsr3 5196  axrrecex 5256  ltmullem 5614  prodge0 5776  nnind 5885  sup2 5998  nnunb 6017  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  uzind 6153  elioc2t 6322  elico2t 6323  elicc2t 6324  caucvglem4 7096  efseq0ex 7253  infdif2 7512  tgclt 7566  ubthlem6 8465  chsscm 9033  occont 9076  chintcl 9210  shless 9262  h1de2 9391  spansnm0 9512  strlem1 10087  mdslmd1 10164  uninqs 10342  qusp 10430

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain