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  4630  unielrel  5290  ovmpos  6177  caofrss  6298  caoftrn  6299  f1o2ndf1  6424  nnaord  6742  nnmord  6750  oviec  6875  pmss12g  6909  fiss  7264  pm54.43  7487  ltsopi  7635  lttrsr  8077  ltsosr  8079  aptisr  8094  mulextsr1  8096  axpre-mulext  8203  axltwlin  8341  axlttrn  8342  axltadd  8343  axmulgt0  8345  letr  8356  eqord1  8757  remulext1  8873  mulext1  8886  recexap  8927  prodge0  9128  lt2msq  9160  nnge1  9260  zltp1le  9632  uzss  9875  eluzp1m1  9878  xrletr  10141  ixxssixx  10235  zesq  11020  expcanlem  11077  expcan  11078  nn0opthd  11084  wrdind  11414  wrd2ind  11415  pfxccatin12lem3  11424  maxleast  11898  climshftlemg  11987  dvds1lem  12488  bezoutlemzz  12698  algcvg  12745  eucalgcvga  12755  rpexp12i  12852  crth  12921  pc2dvds  13028  pcmpt  13041  prmpwdvds  13053  1arith  13065  ercpbl  13544  insubm  13698  subginv  13898  rngpropd  14099  dvdsunit  14257  subrgdvds  14380  tgss  14928  neipsm  15019  ssrest  15047  cos11  15718  lgsdir2lem4  15904  gausslemma2dlem1a  15931  m1lgs  15958