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  5454  riotaeqimp  7339  f2ndres  7956  frxp2  8084  elixpsn  8875  xpfir  9168  ordiso2  9420  dju1en  10085  iunfo  10452  fpwwe2lem12  10556  canthwelem  10564  axpre-sup  11083  hashbclem  14405  repswfsts  14734  lcmfledvds  16592  lcmfun  16605  coprmprod  16621  coprmproddvdslem  16622  4sqlem19  16925  vdwlem13  16955  clatlem  18459  clatlubcl2  18461  clatglbcl2  18463  gass  19267  gsumcom3fi  19945  lspval  20965  sraval  21165  lindfind  21791  lindsind  21792  aspval  21847  mdetunilem7  22601  opnnei  23103  dfac14  23601  isufil2  23891  metustexhalf  24539  mbfconstlem  25612  dvradcnv  26404  conway  27789  nbupgrel  29432  wspthnonp  29945  htthlem  31006  fprodex01  32917  archiabl  33279  rprmdvdsprod  33617  esplyind  33759  sigapildsys  34346  mrsubvrs  35750  weiunlem  36691  ttcwf2  36753  fvineqsneq  37774  ftc1anclem6  38065  pclfinclN  40442  diaval  41524  docavalN  41615  dochval  41843  dochexmidlem8  41959  unitscyglem4  42683  uzwo4  45501  iblcncfioo  46421  stoweidlem17  46460  stirlinglem10  46526  fourierdlem62  46611  fourierdlem63  46612  fourierdlem65  46614  fourierdlem73  46622  fourierdlem80  46629  fourierdlem82  46631  fourierdlem101  46650  ioorrnopn  46748  ioorrnopnxr  46750  salexct  46777  sge0fodjrnlem  46859  ismeannd  46910  voliunsge0lem  46915  carageneld  46945  ovncvrrp  47007  iinhoiicc  47117  vonioo  47125  vonicc  47128  tz6.12-afv  47636  iccpartiltu  47897  rrx2pnecoorneor  49206  intubeu  49474  unilbeu  49475