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  4635  unielrel  5295  ovmpos  6185  caofrss  6307  caoftrn  6308  f1o2ndf1  6437  nnaord  6755  nnmord  6763  oviec  6888  pmss12g  6922  fiss  7277  pm54.43  7500  ltsopi  7651  lttrsr  8093  ltsosr  8095  aptisr  8110  mulextsr1  8112  axpre-mulext  8219  axltwlin  8357  axlttrn  8358  axltadd  8359  axmulgt0  8361  letr  8372  eqord1  8774  remulext1  8890  mulext1  8903  recexap  8944  prodge0  9145  lt2msq  9177  nnge1  9277  zltp1le  9649  uzss  9893  eluzp1m1  9896  xrletr  10160  ixxssixx  10254  zesq  11045  expcanlem  11102  expcan  11103  nn0opthd  11109  wrdind  11439  wrd2ind  11440  pfxccatin12lem3  11449  maxleast  11923  climshftlemg  12012  dvds1lem  12513  bezoutlemzz  12723  algcvg  12770  eucalgcvga  12780  rpexp12i  12877  crth  12946  pc2dvds  13053  pcmpt  13066  prmpwdvds  13078  1arith  13090  ercpbl  13595  insubm  13740  subginv  13934  rngpropd  14194  dvdsunit  14357  subrgdvds  14481  tgss  15054  neipsm  15145  ssrest  15173  cos11  15844  lgsdir2lem4  16030  gausslemma2dlem1a  16057  m1lgs  16084