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  5485  riotaeqimp  7403  f2ndres  8026  frxp2  8161  elixpsn  8966  xpfir  9260  ordiso2  9510  dju1en  10251  iunfo  10624  fpwwe2lem12  10728  canthwelem  10736  axpre-sup  11255  hashbclem  14598  repswfsts  14933  lcmfledvds  16808  lcmfun  16821  coprmprod  16837  coprmproddvdslem  16838  4sqlem19  17142  vdwlem13  17172  clatlem  18677  clatlubcl2  18679  clatglbcl2  18681  gass  19516  gsumcom3fi  20194  lspval  21251  sraval  21451  lindfind  22123  lindsind  22124  aspval  22181  mdetunilem7  22934  opnnei  23439  dfac14  23938  isufil2  24228  metustexhalf  24876  mbfconstlem  25949  dvradcnv  26749  conway  28166  nbupgrel  29927  wspthnonp  30449  htthlem  31520  fprodex01  33459  archiabl  33802  rprmdvdsprod  34109  esplyind  34250  sigapildsys  34838  mrsubvrs  36356  weiunlem  37326  ttcwf2  37388  fvineqsneq  38411  ftc1anclem6  38692  negprop  38719  impprop  38720  pclfinclN  41083  diaval  42165  docavalN  42256  dochval  42484  dochexmidlem8  42600  unitscyglem4  43324  uzwo4  46146  iblcncfioo  47064  stoweidlem17  47103  stirlinglem10  47169  fourierdlem62  47254  fourierdlem63  47255  fourierdlem65  47257  fourierdlem73  47265  fourierdlem80  47272  fourierdlem82  47274  fourierdlem101  47293  ioorrnopn  47391  ioorrnopnxr  47393  salexct  47420  sge0fodjrnlem  47502  ismeannd  47553  voliunsge0lem  47558  carageneld  47588  ovncvrrp  47650  iinhoiicc  47760  vonioo  47768  vonicc  47771  tz6.12-afv  48319  iccpartiltu  48580  rrx2pnecoorneor  49903  intubeu  50168  unilbeu  50169