Theorem 3imtr4g 552

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 551	1 |- (ph -> (th -> ta))

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

This theorem is referenced by:  pm3.48 556  pm5.74 582  ordi 595  3anim123d 898  3orim123d 899  19.22 1037  hbbid 1110  a12stdy1 1370  a12studyALT 1377  immo 1415  moimv 1417  2euswap 1443  hbabd 1466  r19.20 1699  r19.20da 1705  r19.20dv2 1708  r19.22dv2 1733  moeq3 1917  2reuswap 1933  hbcsb1g 2020  hbcsbg 2022  ssel 2059  sstr2 2067  sscon 2167  ssdif 2168  unss1 2195  ssrin 2230  difin0ss 2328  r19.2z 2343  prel12 2480  ssuni 2517  intss 2549  intssuni 2550  ss2iun 2572  iununi 2611  ssbrd 2651  sspwb 2750  poss 2836  soss 2847  frss 2916  dfwe2 2930  wess 2931  onint 3001  orduniorsuc 3082  nnsuc 3143  finds 3151  finds2 3153  relss 3241  ssxp 3251  relop 3270  cnvss 3286  dmss 3305  dffun7 3532  fun 3632  isomin 3890  f1oweALT 3897  tz7.48lem 3946  tz7.48-3 3949  oaass 4185  ss2ixp 4344  xpdom2 4428  ensdomtr 4457  domsdomtr 4462  mapenlem2 4476  mapdom2 4480  ssenen 4490  pssnn 4519  ssnn 4520  r1pwcl 4667  zorn2lem4 4771  zorn2lem7 4774  ondomon 4836  alephval3 4883  cfub 4888  1pr 5097  addclprlem2 5099  distrlem1pr 5107  psslinpr 5115  ltexprlem3 5124  ltexprlem4 5125  reclem2pr 5137  suplem1pr 5141  suppsr2 5203  suppsr3 5204  axrrecex 5264  ltmullem 5622  prodge0 5784  nnind 5893  sup2 6006  nnunb 6025  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  uzind 6161  elioc2t 6330  elico2t 6331  elicc2t 6332  caucvglem4 7104  efseq0ex 7261  infdif2 7520  tgclt 7574  ubthlem6 8478  chsscm 9051  occont 9099  chintcl 9233  shless 9285  h1de2 9414  spansnm0 9535  strlem1 10115  mdslmd1 10193  uninqs 10378  qusp 10466

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