Theorem syl5bir 152

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3g  203  19.37-1  1633  mo3h  2026  necon1bidc  2332  necon4aidc  2348  ceqex  2780  ssdisj  3383  ralidm  3427  exmid1dc  4081  rexxfrd  4342  sucprcreg  4422  imain  5161  f0rn0  5273  funopfv  5413  mpteqb  5463  funfvima  5601  fliftfun  5649  iinerm  6453  eroveu  6472  th3qlem1  6483  updjudhf  6914  elni2  7064  genpdisj  7273  lttri3  7761  zfz1iso  10471  cau3lem  10772  maxleast  10871  rexanre  10878  climcau  11002  summodc  11038  mertenslem2  11191  divgcdcoprmex  11623  prmind2  11641  opnneiid  12170  txuni2  12261  txbas  12263  txbasval  12272  txlm  12284  blin2  12415  tgqioo  12527