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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  onsucelsucr  4432  unielrel  5074  ovmpos  5902  caofrss  6014  caoftrn  6015  f1o2ndf1  6133  nnaord  6413  nnmord  6421  oviec  6543  pmss12g  6577  fiss  6873  pm54.43  7063  ltsopi  7152  lttrsr  7594  ltsosr  7596  aptisr  7611  mulextsr1  7613  axpre-mulext  7720  axltwlin  7856  axlttrn  7857  axltadd  7858  axmulgt0  7860  letr  7871  eqord1  8269  remulext1  8385  mulext1  8398  recexap  8438  prodge0  8636  lt2msq  8668  nnge1  8767  zltp1le  9132  uzss  9370  eluzp1m1  9373  xrletr  9621  ixxssixx  9715  zesq  10441  expcanlem  10493  expcan  10494  nn0opthd  10500  maxleast  11017  climshftlemg  11103  dvds1lem  11540  bezoutlemzz  11726  algcvg  11765  eucalgcvga  11775  rpexp12i  11869  crth  11936  tgss  12271  neipsm  12362  ssrest  12390  cos11  12982