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  4574  unielrel  5229  ovmpos  6092  caofrss  6213  caoftrn  6214  f1o2ndf1  6337  nnaord  6618  nnmord  6626  oviec  6751  pmss12g  6785  fiss  7105  pm54.43  7324  ltsopi  7468  lttrsr  7910  ltsosr  7912  aptisr  7927  mulextsr1  7929  axpre-mulext  8036  axltwlin  8175  axlttrn  8176  axltadd  8177  axmulgt0  8179  letr  8190  eqord1  8591  remulext1  8707  mulext1  8720  recexap  8761  prodge0  8962  lt2msq  8994  nnge1  9094  zltp1le  9462  uzss  9704  eluzp1m1  9707  xrletr  9965  ixxssixx  10059  zesq  10840  expcanlem  10897  expcan  10898  nn0opthd  10904  wrdind  11213  wrd2ind  11214  pfxccatin12lem3  11223  maxleast  11639  climshftlemg  11728  dvds1lem  12228  bezoutlemzz  12438  algcvg  12485  eucalgcvga  12495  rpexp12i  12592  crth  12661  pc2dvds  12768  pcmpt  12781  prmpwdvds  12793  1arith  12805  ercpbl  13278  insubm  13432  subginv  13632  rngpropd  13832  dvdsunit  13989  subrgdvds  14112  tgss  14650  neipsm  14741  ssrest  14769  cos11  15440  lgsdir2lem4  15623  gausslemma2dlem1a  15650  m1lgs  15677