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  4612  unielrel  5271  ovmpos  6155  caofrss  6276  caoftrn  6277  f1o2ndf1  6402  nnaord  6720  nnmord  6728  oviec  6853  pmss12g  6887  fiss  7236  pm54.43  7455  ltsopi  7600  lttrsr  8042  ltsosr  8044  aptisr  8059  mulextsr1  8061  axpre-mulext  8168  axltwlin  8306  axlttrn  8307  axltadd  8308  axmulgt0  8310  letr  8321  eqord1  8722  remulext1  8838  mulext1  8851  recexap  8892  prodge0  9093  lt2msq  9125  nnge1  9225  zltp1le  9595  uzss  9838  eluzp1m1  9841  xrletr  10104  ixxssixx  10198  zesq  10983  expcanlem  11040  expcan  11041  nn0opthd  11047  wrdind  11369  wrd2ind  11370  pfxccatin12lem3  11379  maxleast  11853  climshftlemg  11942  dvds1lem  12443  bezoutlemzz  12653  algcvg  12700  eucalgcvga  12710  rpexp12i  12807  crth  12876  pc2dvds  12983  pcmpt  12996  prmpwdvds  13008  1arith  13020  ercpbl  13494  insubm  13648  subginv  13848  rngpropd  14049  dvdsunit  14207  subrgdvds  14330  tgss  14874  neipsm  14965  ssrest  14993  cos11  15664  lgsdir2lem4  15850  gausslemma2dlem1a  15877  m1lgs  15904