Theorem 3imtr4g 564

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

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

This theorem is referenced by:  pm3.48 568  pm5.74 594  ordi 607  3anim123d 912  3orim123d 913  19.22 1080  hbbid 1153  a12stdy1 1414  a12studyALT 1421  immo 1459  moimv 1461  2euswap 1488  hbabd 1514  r19.20 1749  r19.20da 1755  r19.20dv2 1758  r19.22dv2 1783  moeq3 1968  2reuswap 1984  hbcsb1g 2075  hbcsbg 2077  ssel 2114  sstr2 2122  sscon 2222  ssdif 2223  unss1 2250  ssrin 2285  difin0ss 2384  r19.2z 2399  prel12 2538  ssuni 2576  intss 2608  intssuni 2609  ss2iun 2631  iununi 2671  ssbrd 2711  sspwb 2811  poss 2897  soss 2908  frss 2978  dfwe2 2992  wess 2993  onint 3063  orduniorsuc 3144  finds 3213  finds2 3215  relss 3303  ssxp 3313  relop 3332  cnvss 3348  dmss 3367  dffun7 3597  fun 3698  isomin 3957  f1oweALT 3964  tz7.48lem 4013  tz7.48-3 4016  oaass 4253  ss2ixp 4415  xpdom2 4505  ensdomtr 4534  domsdomtr 4539  mapenlem2 4555  mapdom2 4559  ssenen 4569  pssnn 4599  r1pwcl 4749  zorn2lem4 4853  zorn2lem7 4856  ondomon 4921  cfub 4973  1pr 5182  addclprlem2 5184  distrlem1pr 5192  psslinpr 5200  ltexprlem3 5209  ltexprlem4 5210  reclem2pr 5222  suplem1pr 5226  suppsr2 5288  suppsr3 5289  axrrecex 5349  ltmullem 5705  prodge0i 5878  nnind 5997  sup2 6133  nnunb 6152  xrsupsslem 6158  xrinfmsslem 6159  supxrre 6165  uzind 6290  elioc2 6415  elico2 6416  elicc2 6417  caucvglem4 7250  efseq0ex 7401  infdif2 7661  tgcl 7713  ubthlem6 8618  chsscmi 9195  occon 9243  chintcli 9378  shlessi 9430  h1de2i 9559  spansnm0i 9678  strlem1 10261  mdslmd1i 10340  uninqs 10527  eqindhome 10635  qusp 10649

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 154  df-an 232

Copyright terms: Public domain