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  4612  unielrel  5271  ovmpos  6155  caofrss  6276  caoftrn  6277  f1o2ndf1  6402  nnaord  6720  nnmord  6728  oviec  6853  pmss12g  6887  fiss  7219  pm54.43  7438  ltsopi  7583  lttrsr  8025  ltsosr  8027  aptisr  8042  mulextsr1  8044  axpre-mulext  8151  axltwlin  8289  axlttrn  8290  axltadd  8291  axmulgt0  8293  letr  8304  eqord1  8705  remulext1  8821  mulext1  8834  recexap  8875  prodge0  9076  lt2msq  9108  nnge1  9208  zltp1le  9578  uzss  9821  eluzp1m1  9824  xrletr  10087  ixxssixx  10181  zesq  10966  expcanlem  11023  expcan  11024  nn0opthd  11030  wrdind  11352  wrd2ind  11353  pfxccatin12lem3  11362  maxleast  11836  climshftlemg  11925  dvds1lem  12426  bezoutlemzz  12636  algcvg  12683  eucalgcvga  12693  rpexp12i  12790  crth  12859  pc2dvds  12966  pcmpt  12979  prmpwdvds  12991  1arith  13003  ercpbl  13477  insubm  13631  subginv  13831  rngpropd  14032  dvdsunit  14190  subrgdvds  14313  tgss  14857  neipsm  14948  ssrest  14976  cos11  15647  lgsdir2lem4  15833  gausslemma2dlem1a  15860  m1lgs  15887