Theorem 3imtr4g 426

Description: More general version of 3imtr4 192. 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 150	. 2 |- (ps <-> th)
4		3imtr4g.3	. . 3 |- (ta <-> ch)
5	4	bicomi 150	. 2 |- (ch <-> ta )
6	1, 3, 5	3imtr3g 425	1 |- (ph -> (th -> ta ))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  pm3.48 430  pm5.74 442  ordi 452  im3ord 637  19.22 722  hbbid 789  del40 839  del41 840  del42 841  del43 856  immo 1043  moimv 1044  2euswap 1065  r19.20 1251  r19.20da 1255  r19.22dv2 1277  2reuswap 1341  moeq3 1432  ssel 1502  sstr2 1510  sscon 1599  ssdif 1600  unss1 1627  ssrin 1661  difin0ss 1753  r19.2z 1766  sspwb 1863  prel12 1875  pwpw0 1883  ssuni 1937  intss 1983  ss2iun 2005  iununi 2037  ssbrd 2094  poss 2129  soss 2140  frss 2173  dfwe2 2187  wess 2188  onint 2261  orduniorsuc 2337  nnsuc 2389  finds 2397  finds2 2399  ssrel 2479  ssxp 2487  cnvss 2512  dmss 2530  dffun7 2688  fun 2763  isomin 2937  f1oweOLD 2944  tz7.48lem 2993  tz7.48-3 2996  oaass 3163  xpdom2 3345  ensdomtr 3372  domsdomtr 3374  mapenlem2 3385  mapdom2 3389  ssenen 3399  pssnn 3428  ssnn 3429  r1pwcl 3530  zornlem4 3606  zornlem7 3609  ondomon 3662  cfub 3703  1pr 3911  addclprlem2 3913  distrlem1pr 3921  psslinpr 3929  ltexprlem3 3938  ltexprlem4 3939  reclem2pr 3951  suplem1pr 3955  suppsr2 4017  suppsr3 4018  axrrecex 4081  ltmullem 4337  nnind 4434  sup2 4510  nnunb 4520  chsscm 5147  occont 5168  occllem6 5185  chintcl 5296  shless 5348  h1de2 5458  strlem1 5691

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org