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 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  onsucelsucr  4655  unielrel  5315  ovmpos  6212  caofrss  6334  caoftrn  6335  f1o2ndf1  6464  nnaord  6782  nnmord  6790  oviec  6915  pmss12g  6956  fiss  7311  pm54.43  7536  ltsopi  7687  lttrsr  8129  ltsosr  8131  aptisr  8146  mulextsr1  8148  axpre-mulext  8255  axltwlin  8393  axlttrn  8394  axltadd  8395  axmulgt0  8397  letr  8408  eqord1  8811  remulext1  8927  mulext1  8940  recexap  8981  prodge0  9184  lt2msq  9216  nnge1  9327  zltp1le  9699  uzss  9943  eluzp1m1  9946  xrletr  10210  ixxssixx  10304  zesq  11096  expcanlem  11153  expcan  11154  nn0opthd  11160  wrdind  11494  wrd2ind  11495  pfxccatin12lem3  11504  maxleast  11979  climshftlemg  12068  dvds1lem  12569  bezoutlemzz  12779  algcvg  12826  eucalgcvga  12836  rpexp12i  12933  crth  13002  pc2dvds  13109  pcmpt  13122  prmpwdvds  13134  1arith  13146  ercpbl  13652  insubm  13792  subginv  13984  rngpropd  14254  dvdsunit  14419  subrgdvds  14543  tgss  15164  neipsm  15255  ssrest  15283  cos11  15954  lgsdir2lem4  16150  gausslemma2dlem1a  16177  m1lgs  16204