Theorem birani 509

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 219	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantr 486	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:  sscon34b  4252  preqsnd  4817  f1o00  6883  fompt  7142  fcoconst  7159  nvocnv  7312  ordsson  7821  offsplitfpar  8157  funsssuppss  8235  tposf12  8296  suppssfifsupp  9399  cardmin2  10107  acacni  10246  fnct  10647  fnctOLD  10648  hash7g  14658  relexpindlem  15245  reccn2  15793  coprmproddvdslem  16866  hashbccl  17210  cshwsdisj  17305  clatlem  18705  dfgrp3lem  19277  ressmulgnn0  19316  mulgnngsum  19318  grpissubg  19386  isnzr2hash  20800  cnfldfunALT  21723  submabas  22923  mdetunilem9  22965  smadiadetlem4  23014  slesolinv  23028  mat2pmatmul  23079  mat2pmatlin  23083  decpmatmul  23120  pm2mpf1  23147  indiscld  23439  cnrest2r  23635  2ndcsb  23797  kgenidm  23896  hausflim  24330  metustfbas  24906  vitalilem1  25959  coseq00topi  26861  coseq0negpitopi  26862  cxplogb  27144  atanlogsublem  27273  cusgredg  30035  dfpth2  30344  usgr2pthlem  30379  wspthnonp  30478  elwwlks2ons3im  30573  usgrwwlks2on  30577  umgrwwlks2on  30578  1to3vfriendship  30912  wlkl0  30998  ssmd2  32944  mdslmd1lem2  32958  difeq  33186  1stpreimas  33370  fpwrelmapffs  33396  insiga  34840  eulerpartlemt  35073  signsvtn0  35269  signlem0  35286  bnj927  35470  ordprcon  35793  derangenlem  36103  bccolsum  36682  cntotbnd  38922  dfac21  44261  tfsconcatrev  44542  eliin2f  46324  wessf1ornlem  46405  founiiun0  46410  disjinfi  46412  pimxrneun  46703  islptre  46836  climlimsupcex  46984  wallispi2lem2  47287  stirlinglem12  47300  fourierdlem12  47334  fourierswlem  47445  qndenserrnbllem  47509  dfsalgen2  47556  sge0ltfirp  47615  sge0resplit  47621  hoidmvlelem1  47810  hoidmvlelem3  47812  hoidmvlelem5  47814  hspdifhsp  47831  fresfo  48323  uniimaprimaeqfv  48669  usgrgrtrirex  49253  uspgrlimlem3  49293  grlimedgclnbgr  49298  gpg5gricstgr3  49393  gpgprismgr4cycllem8  49405  lincfsuppcl  49730  lincvalpr  49735  ldepsnlinclem1  49822  ldepsnlinclem2  49823  nn0sumshdiglemB  49937  euendfunc2  50867  incat  50944