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  4239  preqsnd  4797  f1o00  6809  fompt  7066  fcoconst  7083  nvocnv  7232  ordsson  7733  offsplitfpar  8065  funsssuppss  8137  tposf12  8198  suppssfifsupp  9290  cardmin2  9921  acacni  10061  fnct  10457  hash7g  14446  relexpindlem  15023  reccn2  15557  coprmproddvdslem  16629  hashbccl  16972  cshwsdisj  17067  clatlem  18466  dfgrp3lem  19012  ressmulgnn0  19051  mulgnngsum  19053  grpissubg  19120  isnzr2hash  20498  cnfldfunALT  21369  submabas  22568  mdetunilem9  22610  smadiadetlem4  22659  slesolinv  22670  mat2pmatmul  22721  mat2pmatlin  22725  decpmatmul  22762  pm2mpf1  22789  indiscld  23081  cnrest2r  23277  2ndcsb  23439  kgenidm  23537  hausflim  23971  metustfbas  24547  vitalilem1  25600  coseq00topi  26491  coseq0negpitopi  26492  cxplogb  26775  atanlogsublem  26904  cusgredg  29518  dfpth2  29822  usgr2pthlem  29856  wspthnonp  29952  elwwlks2ons3im  30047  usgrwwlks2on  30051  umgrwwlks2on  30052  1to3vfriendship  30376  wlkl0  30462  ssmd2  32408  mdslmd1lem2  32422  difeq  32613  1stpreimas  32805  fpwrelmapffs  32833  insiga  34328  eulerpartlemt  34562  signsvtn0  34761  signlem0  34778  bnj927  34959  derangenlem  35400  bccolsum  35968  cntotbnd  38164  dfac21  43512  tfsconcatrev  43794  eliin2f  45552  wessf1ornlem  45633  founiiun0  45638  disjinfi  45640  pimxrneun  45932  islptre  46065  climlimsupcex  46213  wallispi2lem2  46516  stirlinglem12  46529  fourierdlem12  46563  fourierswlem  46674  qndenserrnbllem  46738  dfsalgen2  46785  sge0ltfirp  46844  sge0resplit  46850  hoidmvlelem1  47039  hoidmvlelem3  47041  hoidmvlelem5  47043  hspdifhsp  47060  fresfo  47512  uniimaprimaeqfv  47858  usgrgrtrirex  48442  uspgrlimlem3  48482  grlimedgclnbgr  48487  gpg5gricstgr3  48582  gpgprismgr4cycllem8  48594  lincfsuppcl  48905  lincvalpr  48910  ldepsnlinclem1  48997  ldepsnlinclem2  48998  nn0sumshdiglemB  49112  euendfunc2  50018  incat  50092