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  1662  mo3h  2067  necon1bidc  2388  necon4aidc  2404  r19.30dc  2613  ceqex  2853  ssdisj  3465  ralidm  3509  exmid1dc  4179  rexxfrd  4441  sucprcreg  4526  imain  5270  f0rn0  5382  funopfv  5526  mpteqb  5576  funfvima  5716  fliftfun  5764  iinerm  6573  eroveu  6592  th3qlem1  6603  updjudhf  7044  elni2  7255  genpdisj  7464  lttri3  7978  nn0ltexp2  10623  zfz1iso  10754  cau3lem  11056  maxleast  11155  rexanre  11162  climcau  11288  summodc  11324  mertenslem2  11477  prodmodclem2  11518  prodmodc  11519  fprodseq  11524  divgcdcoprmex  12034  prmind2  12052  pcqmul  12235  pcxcl  12243  pcadd  12271  mul4sq  12324  opnneiid  12804  txuni2  12896  txbas  12898  txbasval  12907  txlm  12919  blin2  13072  tgqioo  13187  2sqlem5  13595  bj-charfunr  13692