Theorem biranri 508

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 230	. 2 ⊢ (𝜓 → 𝜑)
3	2	adantr 483	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  dminss  6128  f1o00  6831  f1stres  7983  fnse  8101  trcl  9673  grothomex  10777  fzoopth  13758  fseqsupcl  13980  expcl2lem  14076  ipoval  18538  ipolerval  18540  eqgfval  19193  fvmptnn04if  22882  cnpnei  23297  qtopuni  23735  tgqtop  23745  isfild  23891  dvnfval  25957  logbfval  26825  nbusgrvtxm1  29519  clwwlkf1  30190  df3nandALT1  36707  dgraaub  43673  zp1modne  47894