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	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3imtr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3imtr4d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3imtr4d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	sylibrd 169	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 150	1 ⊢ (𝜑 → (𝜃 → 𝜏))

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  4650  unielrel  5310  ovmpos  6202  caofrss  6324  caoftrn  6325  f1o2ndf1  6454  nnaord  6772  nnmord  6780  oviec  6905  pmss12g  6946  fiss  7301  pm54.43  7526  ltsopi  7677  lttrsr  8119  ltsosr  8121  aptisr  8136  mulextsr1  8138  axpre-mulext  8245  axltwlin  8383  axlttrn  8384  axltadd  8385  axmulgt0  8387  letr  8398  eqord1  8801  remulext1  8917  mulext1  8930  recexap  8971  prodge0  9174  lt2msq  9206  nnge1  9306  zltp1le  9678  uzss  9922  eluzp1m1  9925  xrletr  10189  ixxssixx  10283  zesq  11074  expcanlem  11131  expcan  11132  nn0opthd  11138  wrdind  11472  wrd2ind  11473  pfxccatin12lem3  11482  maxleast  11957  climshftlemg  12046  dvds1lem  12547  bezoutlemzz  12757  algcvg  12804  eucalgcvga  12814  rpexp12i  12911  crth  12980  pc2dvds  13087  pcmpt  13100  prmpwdvds  13112  1arith  13124  ercpbl  13629  insubm  13769  subginv  13961  rngpropd  14229  dvdsunit  14392  subrgdvds  14516  tgss  15087  neipsm  15178  ssrest  15206  cos11  15877  lgsdir2lem4  16064  gausslemma2dlem1a  16091  m1lgs  16118