Theorem bilanri 512

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 487	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:  euotd  5494  riotaeqimp  7399  f2ndres  8014  frxp2  8145  elixpsn  8947  xpfir  9241  ordiso2  9490  dju1en  10177  iunfo  10550  fpwwe2lem12  10654  canthwelem  10662  axpre-sup  11181  hashbclem  14519  repswfsts  14854  lcmfledvds  16726  lcmfun  16739  coprmprod  16755  coprmproddvdslem  16756  4sqlem19  17059  vdwlem13  17089  clatlem  18594  clatlubcl2  18596  clatglbcl2  18598  gass  19432  gsumcom3fi  20110  lspval  21163  sraval  21363  lindfind  22033  lindsind  22034  aspval  22091  mdetunilem7  22844  opnnei  23349  dfac14  23848  isufil2  24138  metustexhalf  24786  mbfconstlem  25859  dvradcnv  26657  conway  28045  nbupgrel  29806  wspthnonp  30328  htthlem  31399  fprodex01  33297  archiabl  33640  rprmdvdsprod  33946  esplyind  34087  sigapildsys  34675  mrsubvrs  36103  weiunlem  37084  ttcwf2  37146  fvineqsneq  38168  ftc1anclem6  38449  pclfinclN  40825  diaval  41907  docavalN  41998  dochval  42226  dochexmidlem8  42342  unitscyglem4  43066  uzwo4  45889  iblcncfioo  46808  stoweidlem17  46847  stirlinglem10  46913  fourierdlem62  46998  fourierdlem63  46999  fourierdlem65  47001  fourierdlem73  47009  fourierdlem80  47016  fourierdlem82  47018  fourierdlem101  47037  ioorrnopn  47135  ioorrnopnxr  47137  salexct  47164  sge0fodjrnlem  47246  ismeannd  47297  voliunsge0lem  47302  carageneld  47332  ovncvrrp  47394  iinhoiicc  47504  vonioo  47512  vonicc  47515  tz6.12-afv  48063  iccpartiltu  48324  rrx2pnecoorneor  49647  intubeu  49912  unilbeu  49913