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  4632  unielrel  5292  ovmpos  6179  caofrss  6300  caoftrn  6301  f1o2ndf1  6426  nnaord  6744  nnmord  6752  oviec  6877  pmss12g  6911  fiss  7266  pm54.43  7489  ltsopi  7637  lttrsr  8079  ltsosr  8081  aptisr  8096  mulextsr1  8098  axpre-mulext  8205  axltwlin  8343  axlttrn  8344  axltadd  8345  axmulgt0  8347  letr  8358  eqord1  8759  remulext1  8875  mulext1  8888  recexap  8929  prodge0  9130  lt2msq  9162  nnge1  9262  zltp1le  9634  uzss  9878  eluzp1m1  9881  xrletr  10144  ixxssixx  10238  zesq  11024  expcanlem  11081  expcan  11082  nn0opthd  11088  wrdind  11418  wrd2ind  11419  pfxccatin12lem3  11428  maxleast  11902  climshftlemg  11991  dvds1lem  12492  bezoutlemzz  12702  algcvg  12749  eucalgcvga  12759  rpexp12i  12856  crth  12925  pc2dvds  13032  pcmpt  13045  prmpwdvds  13057  1arith  13069  ercpbl  13561  insubm  13715  subginv  13915  rngpropd  14116  dvdsunit  14274  subrgdvds  14397  tgss  14945  neipsm  15036  ssrest  15064  cos11  15735  lgsdir2lem4  15921  gausslemma2dlem1a  15948  m1lgs  15975