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-mp 5  ax-1 6  ax-2 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  1652  mo3h  2052  necon1bidc  2360  necon4aidc  2376  ceqex  2812  ssdisj  3419  ralidm  3463  exmid1dc  4123  rexxfrd  4384  sucprcreg  4464  imain  5205  f0rn0  5317  funopfv  5461  mpteqb  5511  funfvima  5649  fliftfun  5697  iinerm  6501  eroveu  6520  th3qlem1  6531  updjudhf  6964  elni2  7122  genpdisj  7331  lttri3  7844  zfz1iso  10584  cau3lem  10886  maxleast  10985  rexanre  10992  climcau  11116  summodc  11152  mertenslem2  11305  prodmodclem2  11346  prodmodc  11347  divgcdcoprmex  11783  prmind2  11801  opnneiid  12333  txuni2  12425  txbas  12427  txbasval  12436  txlm  12448  blin2  12601  tgqioo  12716