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  4424  unielrel  5066  ovmpos  5894  caofrss  6006  caoftrn  6007  f1o2ndf1  6125  nnaord  6405  nnmord  6413  oviec  6535  pmss12g  6569  fiss  6865  pm54.43  7046  ltsopi  7128  lttrsr  7570  ltsosr  7572  aptisr  7587  mulextsr1  7589  axpre-mulext  7696  axltwlin  7832  axlttrn  7833  axltadd  7834  axmulgt0  7836  letr  7847  eqord1  8245  remulext1  8361  mulext1  8374  recexap  8414  prodge0  8612  lt2msq  8644  nnge1  8743  zltp1le  9108  uzss  9346  eluzp1m1  9349  xrletr  9591  ixxssixx  9685  zesq  10410  expcanlem  10462  expcan  10463  nn0opthd  10468  maxleast  10985  climshftlemg  11071  efler  11405  dvds1lem  11504  bezoutlemzz  11690  algcvg  11729  eucalgcvga  11739  rpexp12i  11833  crth  11900  tgss  12232  neipsm  12323  ssrest  12351