Theorem 3imtr4d 202

Description: More general version of 3imtr4i 200. 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 168	. 2 |- ( ph -> ( ps -> ta ) )
5	1, 4	sylbid 149	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  onsucelsucr  4479  unielrel  5125  ovmpos  5956  caofrss  6068  caoftrn  6069  f1o2ndf1  6187  nnaord  6468  nnmord  6476  oviec  6598  pmss12g  6632  fiss  6933  pm54.43  7137  ltsopi  7252  lttrsr  7694  ltsosr  7696  aptisr  7711  mulextsr1  7713  axpre-mulext  7820  axltwlin  7957  axlttrn  7958  axltadd  7959  axmulgt0  7961  letr  7972  eqord1  8372  remulext1  8488  mulext1  8501  recexap  8541  prodge0  8740  lt2msq  8772  nnge1  8871  zltp1le  9236  uzss  9477  eluzp1m1  9480  xrletr  9735  ixxssixx  9829  zesq  10562  expcanlem  10617  expcan  10618  nn0opthd  10624  maxleast  11141  climshftlemg  11229  dvds1lem  11728  bezoutlemzz  11920  algcvg  11959  eucalgcvga  11969  rpexp12i  12064  crth  12133  pc2dvds  12238  pcmpt  12250  tgss  12604  neipsm  12695  ssrest  12723  cos11  13315