Theorem 3imtr4d 202

Description: More general version of 3imtr4i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses

Ref	Expression
3imtr4d.1	|- ( ph -> ( ps -> ch ) )
3imtr4d.2	|- ( ph -> ( th <-> ps ) )
3imtr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3imtr4d	|- ( ph -> ( th -> ta ) )

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3imtr4d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3		3imtr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	sylibrd 168	. 2 |- ( ph -> ( ps -> ta ) )
5	1, 4	sylbid 149	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  onsucelsucr  4492  unielrel  5138  ovmpos  5976  caofrss  6085  caoftrn  6086  f1o2ndf1  6207  nnaord  6488  nnmord  6496  oviec  6619  pmss12g  6653  fiss  6954  pm54.43  7167  ltsopi  7282  lttrsr  7724  ltsosr  7726  aptisr  7741  mulextsr1  7743  axpre-mulext  7850  axltwlin  7987  axlttrn  7988  axltadd  7989  axmulgt0  7991  letr  8002  eqord1  8402  remulext1  8518  mulext1  8531  recexap  8571  prodge0  8770  lt2msq  8802  nnge1  8901  zltp1le  9266  uzss  9507  eluzp1m1  9510  xrletr  9765  ixxssixx  9859  zesq  10594  expcanlem  10649  expcan  10650  nn0opthd  10656  maxleast  11177  climshftlemg  11265  dvds1lem  11764  bezoutlemzz  11957  algcvg  12002  eucalgcvga  12012  rpexp12i  12109  crth  12178  pc2dvds  12283  pcmpt  12295  prmpwdvds  12307  1arith  12319  insubm  12703  tgss  12857  neipsm  12948  ssrest  12976  cos11  13568  lgsdir2lem4  13726