Theorem syl5bir 142

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5bir	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 124	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bir.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 28	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr3g  193  19.37-1  1564  mo3h  1953  necon1bidc  2257  necon4aidc  2273  ceqex  2671  ssdisj  3277  ralidm  3321  rexxfrd  4195  sucprcreg  4273  imain  4981  funopfv  5213  mpteqb  5261  funfvima  5390  fliftfun  5436  iinerm  6178  eroveu  6197  th3qlem1  6208  elni2  6412  genpdisj  6621  lttri3  7098  cau3lem  9710  climcau  9866