Theorem 3imtr4d 203

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  onsucelsucr  4501  unielrel  5148  ovmpos  5988  caofrss  6097  caoftrn  6098  f1o2ndf1  6219  nnaord  6500  nnmord  6508  oviec  6631  pmss12g  6665  fiss  6966  pm54.43  7179  ltsopi  7294  lttrsr  7736  ltsosr  7738  aptisr  7753  mulextsr1  7755  axpre-mulext  7862  axltwlin  7999  axlttrn  8000  axltadd  8001  axmulgt0  8003  letr  8014  eqord1  8414  remulext1  8530  mulext1  8543  recexap  8583  prodge0  8784  lt2msq  8816  nnge1  8915  zltp1le  9280  uzss  9521  eluzp1m1  9524  xrletr  9779  ixxssixx  9873  zesq  10608  expcanlem  10663  expcan  10664  nn0opthd  10670  maxleast  11190  climshftlemg  11278  dvds1lem  11777  bezoutlemzz  11970  algcvg  12015  eucalgcvga  12025  rpexp12i  12122  crth  12191  pc2dvds  12296  pcmpt  12308  prmpwdvds  12320  1arith  12332  insubm  12734  tgss  13134  neipsm  13225  ssrest  13253  cos11  13845  lgsdir2lem4  14003