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  4606  unielrel  5264  ovmpos  6144  caofrss  6266  caoftrn  6267  f1o2ndf1  6392  nnaord  6676  nnmord  6684  oviec  6809  pmss12g  6843  fiss  7175  pm54.43  7394  ltsopi  7539  lttrsr  7981  ltsosr  7983  aptisr  7998  mulextsr1  8000  axpre-mulext  8107  axltwlin  8246  axlttrn  8247  axltadd  8248  axmulgt0  8250  letr  8261  eqord1  8662  remulext1  8778  mulext1  8791  recexap  8832  prodge0  9033  lt2msq  9065  nnge1  9165  zltp1le  9533  uzss  9776  eluzp1m1  9779  xrletr  10042  ixxssixx  10136  zesq  10919  expcanlem  10976  expcan  10977  nn0opthd  10983  wrdind  11302  wrd2ind  11303  pfxccatin12lem3  11312  maxleast  11773  climshftlemg  11862  dvds1lem  12362  bezoutlemzz  12572  algcvg  12619  eucalgcvga  12629  rpexp12i  12726  crth  12795  pc2dvds  12902  pcmpt  12915  prmpwdvds  12927  1arith  12939  ercpbl  13413  insubm  13567  subginv  13767  rngpropd  13967  dvdsunit  14125  subrgdvds  14248  tgss  14786  neipsm  14877  ssrest  14905  cos11  15576  lgsdir2lem4  15759  gausslemma2dlem1a  15786  m1lgs  15813