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  4525  unielrel  5174  ovmpos  6020  caofrss  6131  caoftrn  6132  f1o2ndf1  6253  nnaord  6534  nnmord  6542  oviec  6667  pmss12g  6701  fiss  7006  pm54.43  7219  ltsopi  7349  lttrsr  7791  ltsosr  7793  aptisr  7808  mulextsr1  7810  axpre-mulext  7917  axltwlin  8055  axlttrn  8056  axltadd  8057  axmulgt0  8059  letr  8070  eqord1  8470  remulext1  8586  mulext1  8599  recexap  8640  prodge0  8841  lt2msq  8873  nnge1  8972  zltp1le  9337  uzss  9578  eluzp1m1  9581  xrletr  9838  ixxssixx  9932  zesq  10670  expcanlem  10727  expcan  10728  nn0opthd  10734  maxleast  11254  climshftlemg  11342  dvds1lem  11841  bezoutlemzz  12035  algcvg  12080  eucalgcvga  12090  rpexp12i  12187  crth  12256  pc2dvds  12362  pcmpt  12375  prmpwdvds  12387  1arith  12399  ercpbl  12807  insubm  12937  subginv  13120  rngpropd  13309  dvdsunit  13462  subrgdvds  13582  tgss  14023  neipsm  14114  ssrest  14142  cos11  14734  lgsdir2lem4  14893  m1lgs  14913