Theorem 3imtr4d 201

Description: More general version of 3imtr4i 199. 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 167	. 2 |- ( ph -> ( ps -> ta ) )
5	1, 4	sylbid 148	1 |- ( ph -> ( th -> ta ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  onsucelsucr  4298  unielrel  4924  ovmpt2s  5725  caofrss  5836  caoftrn  5837  f1o2ndf1  5950  nnaord  6220  nnmord  6228  oviec  6350  pmss12g  6384  pm54.43  6762  ltsopi  6823  lttrsr  7252  ltsosr  7254  aptisr  7268  mulextsr1  7270  axpre-mulext  7367  axltwlin  7498  axlttrn  7499  axltadd  7500  axmulgt0  7502  letr  7512  remulext1  8017  mulext1  8030  recexap  8061  prodge0  8250  lt2msq  8282  nnge1  8380  zltp1le  8737  uzss  8971  eluzp1m1  8974  xrletr  9205  ixxssixx  9252  zesq  9968  expcanlem  10020  expcan  10021  nn0opthd  10026  maxleast  10541  climshftlemg  10583  dvds1lem  10682  bezoutlemzz  10866  ialgcvg  10905  eucialgcvga  10915  rpexp12i  11009  crth  11075