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  4544  unielrel  5197  ovmpos  6046  caofrss  6162  caoftrn  6163  f1o2ndf1  6286  nnaord  6567  nnmord  6575  oviec  6700  pmss12g  6734  fiss  7043  pm54.43  7257  ltsopi  7387  lttrsr  7829  ltsosr  7831  aptisr  7846  mulextsr1  7848  axpre-mulext  7955  axltwlin  8094  axlttrn  8095  axltadd  8096  axmulgt0  8098  letr  8109  eqord1  8510  remulext1  8626  mulext1  8639  recexap  8680  prodge0  8881  lt2msq  8913  nnge1  9013  zltp1le  9380  uzss  9622  eluzp1m1  9625  xrletr  9883  ixxssixx  9977  zesq  10750  expcanlem  10807  expcan  10808  nn0opthd  10814  maxleast  11378  climshftlemg  11467  dvds1lem  11967  bezoutlemzz  12169  algcvg  12216  eucalgcvga  12226  rpexp12i  12323  crth  12392  pc2dvds  12499  pcmpt  12512  prmpwdvds  12524  1arith  12536  ercpbl  12974  insubm  13117  subginv  13311  rngpropd  13511  dvdsunit  13668  subrgdvds  13791  tgss  14299  neipsm  14390  ssrest  14418  cos11  15089  lgsdir2lem4  15272  gausslemma2dlem1a  15299  m1lgs  15326