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  6104  f1o00  6802  f1stres  7955  fnse  8073  trcl  9640  grothomex  10743  fzoopth  13708  fseqsupcl  13930  expcl2lem  14026  ipoval  18487  ipolerval  18489  eqgfval  19142  fvmptnn04if  22832  cnpnei  23247  qtopuni  23685  tgqtop  23695  isfild  23841  dvnfval  25907  logbfval  26772  nbusgrvtxm1  29466  clwwlkf1  30137  df3nandALT1  36627  dgraaub  43593  zp1modne  47815