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  5496  riotaeqimp  7393  f2ndres  8010  frxp2  8139  elixpsn  8934  xpfir  9227  ordiso2  9476  dju1en  10154  iunfo  10522  fpwwe2lem12  10626  canthwelem  10634  axpre-sup  11153  hashbclem  14489  repswfsts  14818  lcmfledvds  16689  lcmfun  16702  coprmprod  16718  coprmproddvdslem  16719  4sqlem19  17022  vdwlem13  17052  clatlem  18557  clatlubcl2  18559  clatglbcl2  18561  gass  19370  gsumcom3fi  20048  lspval  21075  sraval  21275  lindfind  21945  lindsind  21946  aspval  22001  mdetunilem7  22754  opnnei  23256  dfac14  23754  isufil2  24044  metustexhalf  24692  mbfconstlem  25765  dvradcnv  26560  conway  27948  nbupgrel  29661  wspthnonp  30174  htthlem  31235  fprodex01  33135  archiabl  33484  rprmdvdsprod  33790  esplyind  33931  sigapildsys  34518  mrsubvrs  35980  weiunlem  36940  ttcwf2  37002  fvineqsneq  38024  ftc1anclem6  38315  pclfinclN  40692  diaval  41774  docavalN  41865  dochval  42093  dochexmidlem8  42209  unitscyglem4  42933  uzwo4  45743  iblcncfioo  46662  stoweidlem17  46701  stirlinglem10  46767  fourierdlem62  46852  fourierdlem63  46853  fourierdlem65  46855  fourierdlem73  46863  fourierdlem80  46870  fourierdlem82  46872  fourierdlem101  46891  ioorrnopn  46989  ioorrnopnxr  46991  salexct  47018  sge0fodjrnlem  47100  ismeannd  47151  voliunsge0lem  47156  carageneld  47186  ovncvrrp  47248  iinhoiicc  47358  vonioo  47366  vonicc  47369  tz6.12-afv  47877  iccpartiltu  48138  rrx2pnecoorneor  49462  intubeu  49729  unilbeu  49730