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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  onsucelsucr  4655  unielrel  5315  ovmpos  6212  caofrss  6334  caoftrn  6335  f1o2ndf1  6464  nnaord  6782  nnmord  6790  oviec  6915  pmss12g  6956  fiss  7311  pm54.43  7537  ltsopi  7688  lttrsr  8130  ltsosr  8132  aptisr  8147  mulextsr1  8149  axpre-mulext  8256  axltwlin  8394  axlttrn  8395  axltadd  8396  axmulgt0  8398  letr  8409  eqord1  8813  remulext1  8930  mulext1  8943  recexap  8984  prodge0  9187  lt2msq  9219  nnge1  9330  zltp1le  9704  uzss  9953  eluzp1m1  9956  xrletr  10221  ixxssixx  10315  zesq  11111  expcanlem  11169  expcan  11170  nn0opthd  11176  wrdind  11510  wrd2ind  11511  pfxccatin12lem3  11520  maxleast  11996  climshftlemg  12087  dvds1lem  12588  bezoutlemzz  12798  algcvg  12845  eucalgcvga  12855  rpexp12i  12953  crth  13025  pc2dvds  13132  pcmpt  13145  prmpwdvds  13157  1arith  13169  ercpbl  13705  insubm  13845  subginv  14037  rngpropd  14338  dvdsunit  14503  subrgdvds  14627  tgss  15255  neipsm  15346  ssrest  15374  cos11  16046  bposlem6  16277  lgsdir2lem4  16316  gausslemma2dlem1a  16343  m1lgs  16370