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  4657  unielrel  5318  ovmpos  6215  caofrss  6338  caoftrn  6339  f1o2ndf1  6468  nnaord  6787  nnmord  6795  oviec  6920  pmss12g  6961  fiss  7316  pm54.43  7542  ltsopi  7693  lttrsr  8135  ltsosr  8137  aptisr  8152  mulextsr1  8154  axpre-mulext  8261  axltwlin  8399  axlttrn  8400  axltadd  8401  axmulgt0  8403  letr  8414  eqord1  8818  remulext1  8935  mulext1  8948  recexap  8989  prodge0  9192  lt2msq  9224  nnge1  9336  zltp1le  9708  uzss  9958  eluzp1m1  9961  xrletr  10226  ixxssixx  10320  zesq  11116  expcanlem  11174  expcan  11175  nn0opthd  11181  wrdind  11515  wrd2ind  11516  pfxccatin12lem3  11525  maxleast  12001  climshftlemg  12092  dvds1lem  12593  bezoutlemzz  12803  algcvg  12850  eucalgcvga  12860  rpexp12i  12958  crth  13030  pc2dvds  13137  pcmpt  13150  prmpwdvds  13162  1arith  13174  ercpbl  13710  insubm  13850  subginv  14042  rngpropd  14360  dvdsunit  14527  subrgdvds  14651  tgss  15306  neipsm  15397  ssrest  15425  cos11  16098  bposlem6  16333  lgsdir2lem4  16372  gausslemma2dlem1a  16399  m1lgs  16426