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  4485  unielrel  5131  ovmpos  5965  caofrss  6074  caoftrn  6075  f1o2ndf1  6196  nnaord  6477  nnmord  6485  oviec  6607  pmss12g  6641  fiss  6942  pm54.43  7146  ltsopi  7261  lttrsr  7703  ltsosr  7705  aptisr  7720  mulextsr1  7722  axpre-mulext  7829  axltwlin  7966  axlttrn  7967  axltadd  7968  axmulgt0  7970  letr  7981  eqord1  8381  remulext1  8497  mulext1  8510  recexap  8550  prodge0  8749  lt2msq  8781  nnge1  8880  zltp1le  9245  uzss  9486  eluzp1m1  9489  xrletr  9744  ixxssixx  9838  zesq  10573  expcanlem  10628  expcan  10629  nn0opthd  10635  maxleast  11155  climshftlemg  11243  dvds1lem  11742  bezoutlemzz  11935  algcvg  11980  eucalgcvga  11990  rpexp12i  12087  crth  12156  pc2dvds  12261  pcmpt  12273  prmpwdvds  12285  1arith  12297  tgss  12703  neipsm  12794  ssrest  12822  cos11  13414  lgsdir2lem4  13572