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  6142  f1o00  6860  f1stres  8025  fnse  8150  trcl  9730  grothomex  10915  fzoopth  13898  fseqsupcl  14121  expcl2lem  14217  ipoval  18705  ipolerval  18707  eqgfval  19389  fvmptnn04if  23168  cnpnei  23583  qtopuni  24022  tgqtop  24032  isfild  24178  dvnfval  26243  logbfval  27119  nbusgrvtxm1  29961  clwwlkf1  30641  df3nandALT1  37262  dgraaub  44226  zp1modne  48498