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  6155  f1o00  6883  f1stres  8049  fnse  8177  trcl  9756  grothomex  10941  fzoopth  13924  fseqsupcl  14147  expcl2lem  14243  ipoval  18733  ipolerval  18735  eqgfval  19417  fvmptnn04if  23197  cnpnei  23612  qtopuni  24051  tgqtop  24061  isfild  24207  dvnfval  26272  logbfval  27148  nbusgrvtxm1  29990  clwwlkf1  30670  df3nandALT1  37365  dgraaub  44342  zp1modne  48627