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  4540  unielrel  5193  ovmpos  6042  caofrss  6157  caoftrn  6158  f1o2ndf1  6281  nnaord  6562  nnmord  6570  oviec  6695  pmss12g  6729  fiss  7036  pm54.43  7250  ltsopi  7380  lttrsr  7822  ltsosr  7824  aptisr  7839  mulextsr1  7841  axpre-mulext  7948  axltwlin  8087  axlttrn  8088  axltadd  8089  axmulgt0  8091  letr  8102  eqord1  8502  remulext1  8618  mulext1  8631  recexap  8672  prodge0  8873  lt2msq  8905  nnge1  9005  zltp1le  9371  uzss  9613  eluzp1m1  9616  xrletr  9874  ixxssixx  9968  zesq  10729  expcanlem  10786  expcan  10787  nn0opthd  10793  maxleast  11357  climshftlemg  11445  dvds1lem  11945  bezoutlemzz  12139  algcvg  12186  eucalgcvga  12196  rpexp12i  12293  crth  12362  pc2dvds  12468  pcmpt  12481  prmpwdvds  12493  1arith  12505  ercpbl  12914  insubm  13057  subginv  13251  rngpropd  13451  dvdsunit  13608  subrgdvds  13731  tgss  14231  neipsm  14322  ssrest  14350  cos11  14988  lgsdir2lem4  15147  gausslemma2dlem1a  15174  m1lgs  15192