Theorem 3imtr4d 192

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

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  onsucelsucr  4234  unielrel  4845  ovmpt2s  5624  caofrss  5735  caoftrn  5736  f1o2ndf1  5849  nnaord  6082  nnmord  6090  oviec  6212  ltsopi  6418  lttrsr  6847  ltsosr  6849  aptisr  6863  mulextsr1  6865  axpre-mulext  6962  axltwlin  7087  axlttrn  7088  axltadd  7089  axmulgt0  7091  letr  7101  remulext1  7590  mulext1  7603  recexap  7634  prodge0  7820  lt2msq  7852  nnge1  7937  zltp1le  8298  uzss  8493  eluzp1m1  8496  xrletr  8724  ixxssixx  8771  zesq  9367  climshftlemg  9823  ialgcvg  9887