Theorem birani 504

Description: Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)

Hypothesis

Ref	Expression
birani.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
birani	⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Proof of Theorem birani

Step	Hyp	Ref	Expression
1		birani.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 217	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantr 481	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:  sscon34b  4232  preqsnd  4790  f1o00  6802  fompt  7059  fcoconst  7076  nvocnv  7225  ordsson  7726  offsplitfpar  8058  funsssuppss  8130  tposf12  8191  suppssfifsupp  9283  cardmin2  9914  acacni  10054  fnct  10450  hash7g  14439  relexpindlem  15016  reccn2  15550  coprmproddvdslem  16622  hashbccl  16965  cshwsdisj  17060  clatlem  18459  dfgrp3lem  19005  ressmulgnn0  19044  mulgnngsum  19046  grpissubg  19113  isnzr2hash  20491  cnfldfunALT  21362  submabas  22561  mdetunilem9  22603  smadiadetlem4  22652  slesolinv  22663  mat2pmatmul  22714  mat2pmatlin  22718  decpmatmul  22755  pm2mpf1  22782  indiscld  23074  cnrest2r  23270  2ndcsb  23432  kgenidm  23530  hausflim  23964  metustfbas  24540  vitalilem1  25593  coseq00topi  26484  coseq0negpitopi  26485  cxplogb  26768  atanlogsublem  26897  cusgredg  29511  dfpth2  29815  usgr2pthlem  29849  wspthnonp  29945  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  1to3vfriendship  30369  wlkl0  30455  ssmd2  32401  mdslmd1lem2  32415  difeq  32606  1stpreimas  32798  fpwrelmapffs  32826  insiga  34321  eulerpartlemt  34555  signsvtn0  34754  signlem0  34771  bnj927  34952  derangenlem  35399  bccolsum  35967  cntotbnd  38163  dfac21  43511  tfsconcatrev  43793  eliin2f  45551  wessf1ornlem  45632  founiiun0  45637  disjinfi  45639  pimxrneun  45931  islptre  46064  climlimsupcex  46212  wallispi2lem2  46515  stirlinglem12  46528  fourierdlem12  46562  fourierswlem  46673  qndenserrnbllem  46737  dfsalgen2  46784  sge0ltfirp  46843  sge0resplit  46849  hoidmvlelem1  47038  hoidmvlelem3  47040  hoidmvlelem5  47042  hspdifhsp  47059  fresfo  47511  uniimaprimaeqfv  47857  usgrgrtrirex  48441  uspgrlimlem3  48481  grlimedgclnbgr  48486  gpg5gricstgr3  48581  gpgprismgr4cycllem8  48593  lincfsuppcl  48904  lincvalpr  48909  ldepsnlinclem1  48996  ldepsnlinclem2  48997  nn0sumshdiglemB  49111  euendfunc2  50017  incat  50091