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  4419  unielrel  5061  ovmpos  5887  caofrss  5999  caoftrn  6000  f1o2ndf1  6118  nnaord  6398  nnmord  6406  oviec  6528  pmss12g  6562  fiss  6858  pm54.43  7039  ltsopi  7121  lttrsr  7563  ltsosr  7565  aptisr  7580  mulextsr1  7582  axpre-mulext  7689  axltwlin  7825  axlttrn  7826  axltadd  7827  axmulgt0  7829  letr  7840  eqord1  8238  remulext1  8354  mulext1  8367  recexap  8407  prodge0  8605  lt2msq  8637  nnge1  8736  zltp1le  9101  uzss  9339  eluzp1m1  9342  xrletr  9584  ixxssixx  9678  zesq  10403  expcanlem  10455  expcan  10456  nn0opthd  10461  maxleast  10978  climshftlemg  11064  efler  11394  dvds1lem  11493  bezoutlemzz  11679  algcvg  11718  eucalgcvga  11728  rpexp12i  11822  crth  11889  tgss  12221  neipsm  12312  ssrest  12340