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  4606  unielrel  5264  ovmpos  6145  caofrss  6267  caoftrn  6268  f1o2ndf1  6393  nnaord  6677  nnmord  6685  oviec  6810  pmss12g  6844  fiss  7176  pm54.43  7395  ltsopi  7540  lttrsr  7982  ltsosr  7984  aptisr  7999  mulextsr1  8001  axpre-mulext  8108  axltwlin  8247  axlttrn  8248  axltadd  8249  axmulgt0  8251  letr  8262  eqord1  8663  remulext1  8779  mulext1  8792  recexap  8833  prodge0  9034  lt2msq  9066  nnge1  9166  zltp1le  9534  uzss  9777  eluzp1m1  9780  xrletr  10043  ixxssixx  10137  zesq  10921  expcanlem  10978  expcan  10979  nn0opthd  10985  wrdind  11307  wrd2ind  11308  pfxccatin12lem3  11317  maxleast  11791  climshftlemg  11880  dvds1lem  12381  bezoutlemzz  12591  algcvg  12638  eucalgcvga  12648  rpexp12i  12745  crth  12814  pc2dvds  12921  pcmpt  12934  prmpwdvds  12946  1arith  12958  ercpbl  13432  insubm  13586  subginv  13786  rngpropd  13987  dvdsunit  14145  subrgdvds  14268  tgss  14806  neipsm  14897  ssrest  14925  cos11  15596  lgsdir2lem4  15779  gausslemma2dlem1a  15806  m1lgs  15833