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  4604  unielrel  5262  ovmpos  6140  caofrss  6262  caoftrn  6263  f1o2ndf1  6388  nnaord  6672  nnmord  6680  oviec  6805  pmss12g  6839  fiss  7167  pm54.43  7386  ltsopi  7530  lttrsr  7972  ltsosr  7974  aptisr  7989  mulextsr1  7991  axpre-mulext  8098  axltwlin  8237  axlttrn  8238  axltadd  8239  axmulgt0  8241  letr  8252  eqord1  8653  remulext1  8769  mulext1  8782  recexap  8823  prodge0  9024  lt2msq  9056  nnge1  9156  zltp1le  9524  uzss  9767  eluzp1m1  9770  xrletr  10033  ixxssixx  10127  zesq  10910  expcanlem  10967  expcan  10968  nn0opthd  10974  wrdind  11293  wrd2ind  11294  pfxccatin12lem3  11303  maxleast  11764  climshftlemg  11853  dvds1lem  12353  bezoutlemzz  12563  algcvg  12610  eucalgcvga  12620  rpexp12i  12717  crth  12786  pc2dvds  12893  pcmpt  12906  prmpwdvds  12918  1arith  12930  ercpbl  13404  insubm  13558  subginv  13758  rngpropd  13958  dvdsunit  14116  subrgdvds  14239  tgss  14777  neipsm  14868  ssrest  14896  cos11  15567  lgsdir2lem4  15750  gausslemma2dlem1a  15777  m1lgs  15804