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  4554  unielrel  5207  ovmpos  6059  caofrss  6180  caoftrn  6181  f1o2ndf1  6304  nnaord  6585  nnmord  6593  oviec  6718  pmss12g  6752  fiss  7061  pm54.43  7280  ltsopi  7415  lttrsr  7857  ltsosr  7859  aptisr  7874  mulextsr1  7876  axpre-mulext  7983  axltwlin  8122  axlttrn  8123  axltadd  8124  axmulgt0  8126  letr  8137  eqord1  8538  remulext1  8654  mulext1  8667  recexap  8708  prodge0  8909  lt2msq  8941  nnge1  9041  zltp1le  9409  uzss  9651  eluzp1m1  9654  xrletr  9912  ixxssixx  10006  zesq  10784  expcanlem  10841  expcan  10842  nn0opthd  10848  maxleast  11443  climshftlemg  11532  dvds1lem  12032  bezoutlemzz  12242  algcvg  12289  eucalgcvga  12299  rpexp12i  12396  crth  12465  pc2dvds  12572  pcmpt  12585  prmpwdvds  12597  1arith  12609  ercpbl  13081  insubm  13235  subginv  13435  rngpropd  13635  dvdsunit  13792  subrgdvds  13915  tgss  14453  neipsm  14544  ssrest  14572  cos11  15243  lgsdir2lem4  15426  gausslemma2dlem1a  15453  m1lgs  15480