Theorem bilanri 511

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 486	1 ⊢ ((𝜒 ∧ 𝜓) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

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 401

This theorem is used by:  euotd  5495  riotaeqimp  7395  f2ndres  8009  frxp2  8138  elixpsn  8933  xpfir  9226  ordiso2  9475  dju1en  10162  iunfo  10529  fpwwe2lem12  10633  canthwelem  10641  axpre-sup  11160  hashbclem  14496  repswfsts  14825  lcmfledvds  16696  lcmfun  16709  coprmprod  16725  coprmproddvdslem  16726  4sqlem19  17029  vdwlem13  17059  clatlem  18564  clatlubcl2  18566  clatglbcl2  18568  gass  19377  gsumcom3fi  20055  lspval  21107  sraval  21307  lindfind  21977  lindsind  21978  aspval  22033  mdetunilem7  22786  opnnei  23288  dfac14  23786  isufil2  24076  metustexhalf  24724  mbfconstlem  25797  dvradcnv  26595  conway  27983  nbupgrel  29706  wspthnonp  30219  htthlem  31280  fprodex01  33180  archiabl  33527  rprmdvdsprod  33833  esplyind  33974  sigapildsys  34561  mrsubvrs  36022  weiunlem  37002  ttcwf2  37064  fvineqsneq  38086  ftc1anclem6  38377  pclfinclN  40752  diaval  41834  docavalN  41925  dochval  42153  dochexmidlem8  42269  unitscyglem4  42993  uzwo4  45801  iblcncfioo  46720  stoweidlem17  46759  stirlinglem10  46825  fourierdlem62  46910  fourierdlem63  46911  fourierdlem65  46913  fourierdlem73  46921  fourierdlem80  46928  fourierdlem82  46930  fourierdlem101  46949  ioorrnopn  47047  ioorrnopnxr  47049  salexct  47076  sge0fodjrnlem  47158  ismeannd  47209  voliunsge0lem  47214  carageneld  47244  ovncvrrp  47306  iinhoiicc  47416  vonioo  47424  vonicc  47427  tz6.12-afv  47938  iccpartiltu  48199  rrx2pnecoorneor  49523  intubeu  49790  unilbeu  49791