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  4505  unielrel  5153  ovmpos  5993  caofrss  6102  caoftrn  6103  f1o2ndf1  6224  nnaord  6505  nnmord  6513  oviec  6636  pmss12g  6670  fiss  6971  pm54.43  7184  ltsopi  7314  lttrsr  7756  ltsosr  7758  aptisr  7773  mulextsr1  7775  axpre-mulext  7882  axltwlin  8019  axlttrn  8020  axltadd  8021  axmulgt0  8023  letr  8034  eqord1  8434  remulext1  8550  mulext1  8563  recexap  8604  prodge0  8805  lt2msq  8837  nnge1  8936  zltp1le  9301  uzss  9542  eluzp1m1  9545  xrletr  9802  ixxssixx  9896  zesq  10631  expcanlem  10686  expcan  10687  nn0opthd  10693  maxleast  11213  climshftlemg  11301  dvds1lem  11800  bezoutlemzz  11993  algcvg  12038  eucalgcvga  12048  rpexp12i  12145  crth  12214  pc2dvds  12319  pcmpt  12331  prmpwdvds  12343  1arith  12355  insubm  12800  subginv  12967  dvdsunit  13180  tgss  13345  neipsm  13436  ssrest  13464  cos11  14056  lgsdir2lem4  14214