Theorem biranri 506

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 229	. 2 ⊢ (𝜓 → 𝜑)
3	2	adantr 481	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  dminss  6111  f1o00  6809  f1stres  7962  fnse  8080  trcl  9647  grothomex  10750  fzoopth  13715  fseqsupcl  13937  expcl2lem  14033  ipoval  18494  ipolerval  18496  eqgfval  19149  fvmptnn04if  22839  cnpnei  23254  qtopuni  23692  tgqtop  23702  isfild  23848  dvnfval  25914  logbfval  26779  nbusgrvtxm1  29473  clwwlkf1  30144  df3nandALT1  36628  dgraaub  43594  zp1modne  47816