Theorem birani 508

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sscon34b  4259  preqsnd  4820  f1o00  6846  fompt  7103  fcoconst  7120  nvocnv  7269  ordsson  7770  offsplitfpar  8102  funsssuppss  8174  tposf12  8235  suppssfifsupp  9328  cardmin2  9973  acacni  10112  fnct  10509  hash7g  14513  relexpindlem  15090  reccn2  15638  coprmproddvdslem  16710  hashbccl  17053  cshwsdisj  17148  clatlem  18548  dfgrp3lem  19095  ressmulgnn0  19134  mulgnngsum  19136  grpissubg  19204  isnzr2hash  20594  cnfldfunALT  21497  submabas  22696  mdetunilem9  22738  smadiadetlem4  22787  slesolinv  22798  mat2pmatmul  22849  mat2pmatlin  22853  decpmatmul  22890  pm2mpf1  22917  indiscld  23209  cnrest2r  23405  2ndcsb  23567  kgenidm  23665  hausflim  24099  metustfbas  24675  vitalilem1  25728  coseq00topi  26625  coseq0negpitopi  26626  cxplogb  26909  atanlogsublem  27038  cusgredg  29683  dfpth2  29987  usgr2pthlem  30021  wspthnonp  30117  elwwlks2ons3im  30212  usgrwwlks2on  30216  umgrwwlks2on  30217  1to3vfriendship  30541  wlkl0  30627  ssmd2  32573  mdslmd1lem2  32587  difeq  32774  1stpreimas  32963  fpwrelmapffs  32991  insiga  34444  eulerpartlemt  34678  signsvtn0  34874  signlem0  34891  bnj927  35075  ordprcon  35393  derangenlem  35534  bccolsum  36102  cntotbnd  38307  dfac21  43655  tfsconcatrev  43937  eliin2f  45680  wessf1ornlem  45761  founiiun0  45766  disjinfi  45768  pimxrneun  46060  islptre  46193  climlimsupcex  46341  wallispi2lem2  46644  stirlinglem12  46657  fourierdlem12  46691  fourierswlem  46802  qndenserrnbllem  46866  dfsalgen2  46913  sge0ltfirp  46972  sge0resplit  46978  hoidmvlelem1  47167  hoidmvlelem3  47169  hoidmvlelem5  47171  hspdifhsp  47188  fresfo  47640  uniimaprimaeqfv  47986  usgrgrtrirex  48570  uspgrlimlem3  48610  grlimedgclnbgr  48615  gpg5gricstgr3  48710  gpgprismgr4cycllem8  48722  lincfsuppcl  49044  lincvalpr  49049  ldepsnlinclem1  49136  ldepsnlinclem2  49137  nn0sumshdiglemB  49251  euendfunc2  50156  incat  50230