Theorem syl5bir 151

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 131	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bir.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3g  202  19.37-1  1604  mo3h  1994  necon1bidc  2297  necon4aidc  2313  ceqex  2722  ssdisj  3300  ralidm  3341  rexxfrd  4213  sucprcreg  4292  imain  5001  funopfv  5234  mpteqb  5282  funfvima  5411  fliftfun  5456  iinerm  6201  eroveu  6220  th3qlem1  6231  elni2  6504  genpdisj  6713  lttri3  7191  cau3lem  10000  maxleast  10099  rexanre  10106  climcau  10184  divgcdcoprmex  10484  prmind2  10502