Theorem biranri 511

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

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

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 402

This theorem is used by:  dminss  6148  f1o00  6857  f1stres  8013  fnse  8134  trcl  9710  grothomex  10841  fzoopth  13820  fseqsupcl  14043  expcl2lem  14139  ipoval  18622  ipolerval  18624  eqgfval  19305  fvmptnn04if  23078  cnpnei  23493  qtopuni  23932  tgqtop  23942  isfild  24088  dvnfval  26154  logbfval  27028  nbusgrvtxm1  29840  clwwlkf1  30520  df3nandALT1  37020  dgraaub  43991  zp1modne  48242