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  4545  unielrel  5198  ovmpos  6050  caofrss  6171  caoftrn  6172  f1o2ndf1  6295  nnaord  6576  nnmord  6584  oviec  6709  pmss12g  6743  fiss  7052  pm54.43  7269  ltsopi  7404  lttrsr  7846  ltsosr  7848  aptisr  7863  mulextsr1  7865  axpre-mulext  7972  axltwlin  8111  axlttrn  8112  axltadd  8113  axmulgt0  8115  letr  8126  eqord1  8527  remulext1  8643  mulext1  8656  recexap  8697  prodge0  8898  lt2msq  8930  nnge1  9030  zltp1le  9397  uzss  9639  eluzp1m1  9642  xrletr  9900  ixxssixx  9994  zesq  10767  expcanlem  10824  expcan  10825  nn0opthd  10831  maxleast  11395  climshftlemg  11484  dvds1lem  11984  bezoutlemzz  12194  algcvg  12241  eucalgcvga  12251  rpexp12i  12348  crth  12417  pc2dvds  12524  pcmpt  12537  prmpwdvds  12549  1arith  12561  ercpbl  13033  insubm  13187  subginv  13387  rngpropd  13587  dvdsunit  13744  subrgdvds  13867  tgss  14383  neipsm  14474  ssrest  14502  cos11  15173  lgsdir2lem4  15356  gausslemma2dlem1a  15383  m1lgs  15410