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 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is used by:  dminss  6149  f1o00  6856  f1stres  8008  fnse  8127  trcl  9695  grothomex  10820  fzoopth  13798  fseqsupcl  14020  expcl2lem  14116  ipoval  18592  ipolerval  18594  eqgfval  19250  fvmptnn04if  23017  cnpnei  23432  qtopuni  23870  tgqtop  23880  isfild  24026  dvnfval  26092  logbfval  26966  nbusgrvtxm1  29740  clwwlkf1  30411  df3nandALT1  36938  dgraaub  43903  zp1modne  48117