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  4600  unielrel  5256  ovmpos  6128  caofrss  6250  caoftrn  6251  f1o2ndf1  6374  nnaord  6655  nnmord  6663  oviec  6788  pmss12g  6822  fiss  7144  pm54.43  7363  ltsopi  7507  lttrsr  7949  ltsosr  7951  aptisr  7966  mulextsr1  7968  axpre-mulext  8075  axltwlin  8214  axlttrn  8215  axltadd  8216  axmulgt0  8218  letr  8229  eqord1  8630  remulext1  8746  mulext1  8759  recexap  8800  prodge0  9001  lt2msq  9033  nnge1  9133  zltp1le  9501  uzss  9743  eluzp1m1  9746  xrletr  10004  ixxssixx  10098  zesq  10880  expcanlem  10937  expcan  10938  nn0opthd  10944  wrdind  11254  wrd2ind  11255  pfxccatin12lem3  11264  maxleast  11724  climshftlemg  11813  dvds1lem  12313  bezoutlemzz  12523  algcvg  12570  eucalgcvga  12580  rpexp12i  12677  crth  12746  pc2dvds  12853  pcmpt  12866  prmpwdvds  12878  1arith  12890  ercpbl  13364  insubm  13518  subginv  13718  rngpropd  13918  dvdsunit  14076  subrgdvds  14199  tgss  14737  neipsm  14828  ssrest  14856  cos11  15527  lgsdir2lem4  15710  gausslemma2dlem1a  15737  m1lgs  15764