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  4564  unielrel  5219  ovmpos  6082  caofrss  6203  caoftrn  6204  f1o2ndf1  6327  nnaord  6608  nnmord  6616  oviec  6741  pmss12g  6775  fiss  7094  pm54.43  7313  ltsopi  7453  lttrsr  7895  ltsosr  7897  aptisr  7912  mulextsr1  7914  axpre-mulext  8021  axltwlin  8160  axlttrn  8161  axltadd  8162  axmulgt0  8164  letr  8175  eqord1  8576  remulext1  8692  mulext1  8705  recexap  8746  prodge0  8947  lt2msq  8979  nnge1  9079  zltp1le  9447  uzss  9689  eluzp1m1  9692  xrletr  9950  ixxssixx  10044  zesq  10825  expcanlem  10882  expcan  10883  nn0opthd  10889  wrdind  11198  wrd2ind  11199  maxleast  11599  climshftlemg  11688  dvds1lem  12188  bezoutlemzz  12398  algcvg  12445  eucalgcvga  12455  rpexp12i  12552  crth  12621  pc2dvds  12728  pcmpt  12741  prmpwdvds  12753  1arith  12765  ercpbl  13238  insubm  13392  subginv  13592  rngpropd  13792  dvdsunit  13949  subrgdvds  14072  tgss  14610  neipsm  14701  ssrest  14729  cos11  15400  lgsdir2lem4  15583  gausslemma2dlem1a  15610  m1lgs  15637