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  6138  f1o00  6848  f1stres  8008  fnse  8128  trcl  9707  grothomex  10886  fzoopth  13866  fseqsupcl  14089  expcl2lem  14185  ipoval  18666  ipolerval  18668  eqgfval  19350  fvmptnn04if  23129  cnpnei  23544  qtopuni  23983  tgqtop  23993  isfild  24139  dvnfval  26204  logbfval  27082  nbusgrvtxm1  29894  clwwlkf1  30574  df3nandALT1  37109  dgraaub  44093  zp1modne  48344