Theorem bilanri 507

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 229	. 2 ⊢ (𝜓 → 𝜑)
3	2	adantl 482	1 ⊢ ((𝜒 ∧ 𝜓) → 𝜑)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  euotd  5461  riotaeqimp  7346  f2ndres  7963  frxp2  8091  elixpsn  8882  xpfir  9175  ordiso2  9427  dju1en  10092  iunfo  10459  fpwwe2lem12  10563  canthwelem  10571  axpre-sup  11090  hashbclem  14412  repswfsts  14741  lcmfledvds  16599  lcmfun  16612  coprmprod  16628  coprmproddvdslem  16629  4sqlem19  16932  vdwlem13  16962  clatlem  18466  clatlubcl2  18468  clatglbcl2  18470  gass  19274  gsumcom3fi  19952  lspval  20972  sraval  21172  lindfind  21798  lindsind  21799  aspval  21854  mdetunilem7  22608  opnnei  23110  dfac14  23608  isufil2  23898  metustexhalf  24546  mbfconstlem  25619  dvradcnv  26411  conway  27796  nbupgrel  29439  wspthnonp  29952  htthlem  31013  fprodex01  32924  archiabl  33286  rprmdvdsprod  33624  esplyind  33766  sigapildsys  34353  mrsubvrs  35751  weiunlem  36692  ttcwf2  36754  fvineqsneq  37775  ftc1anclem6  38066  pclfinclN  40443  diaval  41525  docavalN  41616  dochval  41844  dochexmidlem8  41960  unitscyglem4  42684  uzwo4  45502  iblcncfioo  46422  stoweidlem17  46461  stirlinglem10  46527  fourierdlem62  46612  fourierdlem63  46613  fourierdlem65  46615  fourierdlem73  46623  fourierdlem80  46630  fourierdlem82  46632  fourierdlem101  46651  ioorrnopn  46749  ioorrnopnxr  46751  salexct  46778  sge0fodjrnlem  46860  ismeannd  46911  voliunsge0lem  46916  carageneld  46946  ovncvrrp  47008  iinhoiicc  47118  vonioo  47126  vonicc  47129  tz6.12-afv  47637  iccpartiltu  47898  rrx2pnecoorneor  49207  intubeu  49475  unilbeu  49476