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  4600  unielrel  5256  ovmpos  6134  caofrss  6256  caoftrn  6257  f1o2ndf1  6380  nnaord  6663  nnmord  6671  oviec  6796  pmss12g  6830  fiss  7155  pm54.43  7374  ltsopi  7518  lttrsr  7960  ltsosr  7962  aptisr  7977  mulextsr1  7979  axpre-mulext  8086  axltwlin  8225  axlttrn  8226  axltadd  8227  axmulgt0  8229  letr  8240  eqord1  8641  remulext1  8757  mulext1  8770  recexap  8811  prodge0  9012  lt2msq  9044  nnge1  9144  zltp1le  9512  uzss  9755  eluzp1m1  9758  xrletr  10016  ixxssixx  10110  zesq  10892  expcanlem  10949  expcan  10950  nn0opthd  10956  wrdind  11270  wrd2ind  11271  pfxccatin12lem3  11280  maxleast  11740  climshftlemg  11829  dvds1lem  12329  bezoutlemzz  12539  algcvg  12586  eucalgcvga  12596  rpexp12i  12693  crth  12762  pc2dvds  12869  pcmpt  12882  prmpwdvds  12894  1arith  12906  ercpbl  13380  insubm  13534  subginv  13734  rngpropd  13934  dvdsunit  14092  subrgdvds  14215  tgss  14753  neipsm  14844  ssrest  14872  cos11  15543  lgsdir2lem4  15726  gausslemma2dlem1a  15753  m1lgs  15780