Theorem 3imtr4d 202

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  onsucelsucr  4353  unielrel  4992  ovmpt2s  5806  caofrss  5917  caoftrn  5918  f1o2ndf1  6031  nnaord  6308  nnmord  6316  oviec  6438  pmss12g  6472  pm54.43  6915  ltsopi  6976  lttrsr  7405  ltsosr  7407  aptisr  7421  mulextsr1  7423  axpre-mulext  7520  axltwlin  7651  axlttrn  7652  axltadd  7653  axmulgt0  7655  letr  7665  eqord1  8058  remulext1  8173  mulext1  8186  recexap  8219  prodge0  8412  lt2msq  8444  nnge1  8543  zltp1le  8902  uzss  9138  eluzp1m1  9141  xrletr  9374  ixxssixx  9468  zesq  10187  expcanlem  10239  expcan  10240  nn0opthd  10245  maxleast  10761  climshftlemg  10845  efler  11138  dvds1lem  11234  bezoutlemzz  11418  algcvg  11457  eucalgcvga  11467  rpexp12i  11561  crth  11627  tgss  11915  neipsm  12006  ssrest  12034