Theorem biranri 510

Description: Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)

Hypothesis

Ref	Expression
birani.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biranri	⊢ ((𝜓 ∧ 𝜒) → 𝜑)

Proof of Theorem biranri

Step	Hyp	Ref	Expression
1		birani.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpri 231	. 2 ⊢ (𝜓 → 𝜑)
3	2	adantr 485	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  dminss  6142  f1o00  6846  f1stres  7998  fnse  8117  trcl  9685  grothomex  10802  fzoopth  13782  fseqsupcl  14004  expcl2lem  14100  ipoval  18576  ipolerval  18578  eqgfval  19235  fvmptnn04if  22967  cnpnei  23382  qtopuni  23820  tgqtop  23830  isfild  23976  dvnfval  26042  logbfval  26913  nbusgrvtxm1  29638  clwwlkf1  30309  df3nandALT1  36772  dgraaub  43737  zp1modne  47944