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  4556  unielrel  5210  ovmpos  6069  caofrss  6190  caoftrn  6191  f1o2ndf1  6314  nnaord  6595  nnmord  6603  oviec  6728  pmss12g  6762  fiss  7079  pm54.43  7298  ltsopi  7433  lttrsr  7875  ltsosr  7877  aptisr  7892  mulextsr1  7894  axpre-mulext  8001  axltwlin  8140  axlttrn  8141  axltadd  8142  axmulgt0  8144  letr  8155  eqord1  8556  remulext1  8672  mulext1  8685  recexap  8726  prodge0  8927  lt2msq  8959  nnge1  9059  zltp1le  9427  uzss  9669  eluzp1m1  9672  xrletr  9930  ixxssixx  10024  zesq  10803  expcanlem  10860  expcan  10861  nn0opthd  10867  maxleast  11524  climshftlemg  11613  dvds1lem  12113  bezoutlemzz  12323  algcvg  12370  eucalgcvga  12380  rpexp12i  12477  crth  12546  pc2dvds  12653  pcmpt  12666  prmpwdvds  12678  1arith  12690  ercpbl  13163  insubm  13317  subginv  13517  rngpropd  13717  dvdsunit  13874  subrgdvds  13997  tgss  14535  neipsm  14626  ssrest  14654  cos11  15325  lgsdir2lem4  15508  gausslemma2dlem1a  15535  m1lgs  15562