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  4509  unielrel  5158  ovmpos  6000  caofrss  6109  caoftrn  6110  f1o2ndf1  6231  nnaord  6512  nnmord  6520  oviec  6643  pmss12g  6677  fiss  6978  pm54.43  7191  ltsopi  7321  lttrsr  7763  ltsosr  7765  aptisr  7780  mulextsr1  7782  axpre-mulext  7889  axltwlin  8027  axlttrn  8028  axltadd  8029  axmulgt0  8031  letr  8042  eqord1  8442  remulext1  8558  mulext1  8571  recexap  8612  prodge0  8813  lt2msq  8845  nnge1  8944  zltp1le  9309  uzss  9550  eluzp1m1  9553  xrletr  9810  ixxssixx  9904  zesq  10641  expcanlem  10697  expcan  10698  nn0opthd  10704  maxleast  11224  climshftlemg  11312  dvds1lem  11811  bezoutlemzz  12005  algcvg  12050  eucalgcvga  12060  rpexp12i  12157  crth  12226  pc2dvds  12331  pcmpt  12343  prmpwdvds  12355  1arith  12367  ercpbl  12755  insubm  12877  subginv  13046  dvdsunit  13286  subrgdvds  13361  tgss  13602  neipsm  13693  ssrest  13721  cos11  14313  lgsdir2lem4  14471  m1lgs  14491