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  4557  unielrel  5211  ovmpos  6071  caofrss  6192  caoftrn  6193  f1o2ndf1  6316  nnaord  6597  nnmord  6605  oviec  6730  pmss12g  6764  fiss  7081  pm54.43  7300  ltsopi  7435  lttrsr  7877  ltsosr  7879  aptisr  7894  mulextsr1  7896  axpre-mulext  8003  axltwlin  8142  axlttrn  8143  axltadd  8144  axmulgt0  8146  letr  8157  eqord1  8558  remulext1  8674  mulext1  8687  recexap  8728  prodge0  8929  lt2msq  8961  nnge1  9061  zltp1le  9429  uzss  9671  eluzp1m1  9674  xrletr  9932  ixxssixx  10026  zesq  10805  expcanlem  10862  expcan  10863  nn0opthd  10869  maxleast  11557  climshftlemg  11646  dvds1lem  12146  bezoutlemzz  12356  algcvg  12403  eucalgcvga  12413  rpexp12i  12510  crth  12579  pc2dvds  12686  pcmpt  12699  prmpwdvds  12711  1arith  12723  ercpbl  13196  insubm  13350  subginv  13550  rngpropd  13750  dvdsunit  13907  subrgdvds  14030  tgss  14568  neipsm  14659  ssrest  14687  cos11  15358  lgsdir2lem4  15541  gausslemma2dlem1a  15568  m1lgs  15595