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  5490  riotaeqimp  7426  f2ndres  8050  frxp2  8188  elixpsn  8993  xpfir  9287  ordiso2  9536  dju1en  10277  iunfo  10650  fpwwe2lem12  10754  canthwelem  10762  axpre-sup  11281  hashbclem  14624  repswfsts  14960  lcmfledvds  16836  lcmfun  16849  coprmprod  16865  coprmproddvdslem  16866  4sqlem19  17170  vdwlem13  17200  clatlem  18705  clatlubcl2  18707  clatglbcl2  18709  gass  19545  gsumcom3fi  20223  lspval  21280  sraval  21480  lindfind  22152  lindsind  22153  aspval  22210  mdetunilem7  22963  opnnei  23468  dfac14  23967  isufil2  24257  metustexhalf  24905  mbfconstlem  25978  dvradcnv  26778  conway  28195  nbupgrel  29956  wspthnonp  30478  htthlem  31549  fprodex01  33486  archiabl  33829  rprmdvdsprod  34136  esplyind  34277  sigapildsys  34865  mrsubvrs  36454  weiunlem  37429  ttcwf2  37491  fvineqsneq  38527  ftc1anclem6  38808  negprop  38835  impprop  38836  pclfinclN  41199  diaval  42281  docavalN  42372  dochval  42600  dochexmidlem8  42716  unitscyglem4  43440  uzwo4  46275  iblcncfioo  47193  stoweidlem17  47232  stirlinglem10  47298  fourierdlem62  47383  fourierdlem63  47384  fourierdlem65  47386  fourierdlem73  47394  fourierdlem80  47401  fourierdlem82  47403  fourierdlem101  47422  ioorrnopn  47520  ioorrnopnxr  47522  salexct  47549  sge0fodjrnlem  47631  ismeannd  47682  voliunsge0lem  47687  carageneld  47717  ovncvrrp  47779  iinhoiicc  47889  vonioo  47897  vonicc  47900  tz6.12-afv  48448  iccpartiltu  48709  rrx2pnecoorneor  50033  intubeu  50303  unilbeu  50304  parhomcl2  50950