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  6150  f1o00  6856  f1stres  8009  fnse  8128  trcl  9696  grothomex  10813  fzoopth  13791  fseqsupcl  14013  expcl2lem  14109  ipoval  18585  ipolerval  18587  eqgfval  19243  fvmptnn04if  22985  cnpnei  23400  qtopuni  23838  tgqtop  23848  isfild  23994  dvnfval  26060  logbfval  26931  nbusgrvtxm1  29695  clwwlkf1  30366  df3nandALT1  36876  dgraaub  43845  zp1modne  48056