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  4600  unielrel  5256  ovmpos  6134  caofrss  6256  caoftrn  6257  f1o2ndf1  6380  nnaord  6663  nnmord  6671  oviec  6796  pmss12g  6830  fiss  7155  pm54.43  7374  ltsopi  7518  lttrsr  7960  ltsosr  7962  aptisr  7977  mulextsr1  7979  axpre-mulext  8086  axltwlin  8225  axlttrn  8226  axltadd  8227  axmulgt0  8229  letr  8240  eqord1  8641  remulext1  8757  mulext1  8770  recexap  8811  prodge0  9012  lt2msq  9044  nnge1  9144  zltp1le  9512  uzss  9755  eluzp1m1  9758  xrletr  10016  ixxssixx  10110  zesq  10892  expcanlem  10949  expcan  10950  nn0opthd  10956  wrdind  11269  wrd2ind  11270  pfxccatin12lem3  11279  maxleast  11739  climshftlemg  11828  dvds1lem  12328  bezoutlemzz  12538  algcvg  12585  eucalgcvga  12595  rpexp12i  12692  crth  12761  pc2dvds  12868  pcmpt  12881  prmpwdvds  12893  1arith  12905  ercpbl  13379  insubm  13533  subginv  13733  rngpropd  13933  dvdsunit  14091  subrgdvds  14214  tgss  14752  neipsm  14843  ssrest  14871  cos11  15542  lgsdir2lem4  15725  gausslemma2dlem1a  15752  m1lgs  15779