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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  onsucelsucr  4362  unielrel  5002  ovmpos  5826  caofrss  5937  caoftrn  5938  f1o2ndf1  6055  nnaord  6335  nnmord  6343  oviec  6465  pmss12g  6499  pm54.43  6957  ltsopi  7029  lttrsr  7458  ltsosr  7460  aptisr  7474  mulextsr1  7476  axpre-mulext  7573  axltwlin  7704  axlttrn  7705  axltadd  7706  axmulgt0  7708  letr  7718  eqord1  8112  remulext1  8227  mulext1  8240  recexap  8275  prodge0  8470  lt2msq  8502  nnge1  8601  zltp1le  8960  uzss  9196  eluzp1m1  9199  xrletr  9432  ixxssixx  9526  zesq  10251  expcanlem  10303  expcan  10304  nn0opthd  10309  maxleast  10825  climshftlemg  10910  efler  11203  dvds1lem  11299  bezoutlemzz  11483  algcvg  11522  eucalgcvga  11532  rpexp12i  11626  crth  11692  tgss  12014  neipsm  12105  ssrest  12133