Theorem 3imtr4d 201

Description: More general version of 3imtr4i 199. 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 167	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 148	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  onsucelsucr  4252  unielrel  4865  ovmpt2s  5644  caofrss  5755  caoftrn  5756  f1o2ndf1  5869  nnaord  6105  nnmord  6113  oviec  6235  pm54.43  6459  ltsopi  6510  lttrsr  6939  ltsosr  6941  aptisr  6955  mulextsr1  6957  axpre-mulext  7054  axltwlin  7180  axlttrn  7181  axltadd  7182  axmulgt0  7184  letr  7194  remulext1  7699  mulext1  7712  recexap  7743  prodge0  7932  lt2msq  7964  nnge1  8062  zltp1le  8405  uzss  8639  eluzp1m1  8642  xrletr  8878  ixxssixx  8925  zesq  9591  expcanlem  9643  expcan  9644  nn0opthd  9649  maxleast  10099  climshftlemg  10141  dvds1lem  10206  bezoutlemzz  10391  ialgcvg  10430  eucialgcvga  10440  rpexp12i  10534