Theorem bilanri 509

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
bilanri	⊢ ((𝜒 ∧ 𝜓) → 𝜑)

Proof of Theorem bilanri

Step	Hyp	Ref	Expression
1		birani.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpri 230	. 2 ⊢ (𝜓 → 𝜑)
3	2	adantl 484	1 ⊢ ((𝜒 ∧ 𝜓) → 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  euotd  5476  riotaeqimp  7368  f2ndres  7984  frxp2  8112  elixpsn  8908  xpfir  9201  ordiso2  9453  dju1en  10118  iunfo  10486  fpwwe2lem12  10590  canthwelem  10598  axpre-sup  11117  hashbclem  14455  repswfsts  14784  lcmfledvds  16642  lcmfun  16655  coprmprod  16671  coprmproddvdslem  16672  4sqlem19  16975  vdwlem13  17005  clatlem  18510  clatlubcl2  18512  clatglbcl2  18514  gass  19317  gsumcom3fi  19995  lspval  21015  sraval  21215  lindfind  21841  lindsind  21842  aspval  21897  mdetunilem7  22651  opnnei  23153  dfac14  23651  isufil2  23941  metustexhalf  24589  mbfconstlem  25662  dvradcnv  26454  conway  27842  nbupgrel  29485  wspthnonp  29998  htthlem  31059  fprodex01  32970  archiabl  33332  rprmdvdsprod  33684  esplyind  33826  sigapildsys  34413  mrsubvrs  35820  weiunlem  36771  ttcwf2  36833  fvineqsneq  37854  ftc1anclem6  38145  pclfinclN  40522  diaval  41604  docavalN  41695  dochval  41923  dochexmidlem8  42039  unitscyglem4  42763  uzwo4  45581  iblcncfioo  46500  stoweidlem17  46539  stirlinglem10  46605  fourierdlem62  46690  fourierdlem63  46691  fourierdlem65  46693  fourierdlem73  46701  fourierdlem80  46708  fourierdlem82  46710  fourierdlem101  46729  ioorrnopn  46827  ioorrnopnxr  46829  salexct  46856  sge0fodjrnlem  46938  ismeannd  46989  voliunsge0lem  46994  carageneld  47024  ovncvrrp  47086  iinhoiicc  47196  vonioo  47204  vonicc  47207  tz6.12-afv  47715  iccpartiltu  47976  rrx2pnecoorneor  49285  intubeu  49553  unilbeu  49554