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  5482  riotaeqimp  7391  f2ndres  8009  frxp2  8139  elixpsn  8943  xpfir  9237  ordiso2  9487  dju1en  10222  iunfo  10595  fpwwe2lem12  10699  canthwelem  10707  axpre-sup  11226  hashbclem  14565  repswfsts  14900  lcmfledvds  16770  lcmfun  16783  coprmprod  16799  coprmproddvdslem  16800  4sqlem19  17103  vdwlem13  17133  clatlem  18638  clatlubcl2  18640  clatglbcl2  18642  gass  19477  gsumcom3fi  20155  lspval  21212  sraval  21412  lindfind  22084  lindsind  22085  aspval  22142  mdetunilem7  22895  opnnei  23400  dfac14  23899  isufil2  24189  metustexhalf  24837  mbfconstlem  25910  dvradcnv  26712  conway  28099  nbupgrel  29860  wspthnonp  30382  htthlem  31453  fprodex01  33350  archiabl  33693  rprmdvdsprod  34000  esplyind  34141  sigapildsys  34729  mrsubvrs  36208  weiunlem  37173  ttcwf2  37235  fvineqsneq  38255  ftc1anclem6  38536  negprop  38563  impprop  38564  pclfinclN  40927  diaval  42009  docavalN  42100  dochval  42328  dochexmidlem8  42444  unitscyglem4  43168  uzwo4  45991  iblcncfioo  46910  stoweidlem17  46949  stirlinglem10  47015  fourierdlem62  47100  fourierdlem63  47101  fourierdlem65  47103  fourierdlem73  47111  fourierdlem80  47118  fourierdlem82  47120  fourierdlem101  47139  ioorrnopn  47237  ioorrnopnxr  47239  salexct  47266  sge0fodjrnlem  47348  ismeannd  47399  voliunsge0lem  47404  carageneld  47434  ovncvrrp  47496  iinhoiicc  47606  vonioo  47614  vonicc  47617  tz6.12-afv  48165  iccpartiltu  48426  rrx2pnecoorneor  49749  intubeu  50014  unilbeu  50015