Theorem biimtrrdi 164

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
biimtrrdi.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
biimtrrdi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
biimtrrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrrdi

Step	Hyp	Ref	Expression
1		biimtrrdi.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 158	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	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:  exdistrfor  1824  cbvexdh  1951  repizf2  4214  issref  5074  fnun  5391  ovigg  6079  tfrlem9  6418  tfri3  6466  ordge1n0im  6535  nntri3or  6592  updjud  7199  axprecex  8013  peano5nnnn  8025  peano5nni  9059  zeo  9498  nn0ind-raph  9510  fzm1  10242  fzind2  10390  fzfig  10597  bcpasc  10933  climrecvg1n  11734  oddnn02np1  12266  oddge22np1  12267  evennn02n  12268  evennn2n  12269  bitsfzo  12341  gcdaddm  12380  coprmdvds1  12488  qredeq  12493  fiinopn  14551  zabsle1  15551  incistruhgr  15761  bj-intabssel  15864  triap  16109