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

Proof of Theorem bilanri

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  euotd  5487  riotaeqimp  7383  f2ndres  7999  frxp2  8128  elixpsn  8923  xpfir  9216  ordiso2  9465  dju1en  10143  iunfo  10511  fpwwe2lem12  10615  canthwelem  10623  axpre-sup  11142  hashbclem  14479  repswfsts  14808  lcmfledvds  16680  lcmfun  16693  coprmprod  16709  coprmproddvdslem  16710  4sqlem19  17013  vdwlem13  17043  clatlem  18548  clatlubcl2  18550  clatglbcl2  18552  gass  19362  gsumcom3fi  20040  lspval  21065  sraval  21265  lindfind  21926  lindsind  21927  aspval  21982  mdetunilem7  22736  opnnei  23238  dfac14  23736  isufil2  24026  metustexhalf  24674  mbfconstlem  25747  dvradcnv  26542  conway  27930  nbupgrel  29604  wspthnonp  30117  htthlem  31178  fprodex01  33082  archiabl  33431  rprmdvdsprod  33741  esplyind  33882  sigapildsys  34469  mrsubvrs  35885  weiunlem  36836  ttcwf2  36898  fvineqsneq  37918  ftc1anclem6  38209  pclfinclN  40586  diaval  41668  docavalN  41759  dochval  41987  dochexmidlem8  42103  unitscyglem4  42827  uzwo4  45631  iblcncfioo  46550  stoweidlem17  46589  stirlinglem10  46655  fourierdlem62  46740  fourierdlem63  46741  fourierdlem65  46743  fourierdlem73  46751  fourierdlem80  46758  fourierdlem82  46760  fourierdlem101  46779  ioorrnopn  46877  ioorrnopnxr  46879  salexct  46906  sge0fodjrnlem  46988  ismeannd  47039  voliunsge0lem  47044  carageneld  47074  ovncvrrp  47136  iinhoiicc  47246  vonioo  47254  vonicc  47257  tz6.12-afv  47765  iccpartiltu  48026  rrx2pnecoorneor  49346  intubeu  49613  unilbeu  49614