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  4508  unielrel  5157  ovmpos  5998  caofrss  6107  caoftrn  6108  f1o2ndf1  6229  nnaord  6510  nnmord  6518  oviec  6641  pmss12g  6675  fiss  6976  pm54.43  7189  ltsopi  7319  lttrsr  7761  ltsosr  7763  aptisr  7778  mulextsr1  7780  axpre-mulext  7887  axltwlin  8025  axlttrn  8026  axltadd  8027  axmulgt0  8029  letr  8040  eqord1  8440  remulext1  8556  mulext1  8569  recexap  8610  prodge0  8811  lt2msq  8843  nnge1  8942  zltp1le  9307  uzss  9548  eluzp1m1  9551  xrletr  9808  ixxssixx  9902  zesq  10639  expcanlem  10695  expcan  10696  nn0opthd  10702  maxleast  11222  climshftlemg  11310  dvds1lem  11809  bezoutlemzz  12003  algcvg  12048  eucalgcvga  12058  rpexp12i  12155  crth  12224  pc2dvds  12329  pcmpt  12341  prmpwdvds  12353  1arith  12365  ercpbl  12750  insubm  12872  subginv  13041  dvdsunit  13281  subrgdvds  13356  tgss  13566  neipsm  13657  ssrest  13685  cos11  14277  lgsdir2lem4  14435  m1lgs  14455