Theorem birani 506

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 218	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantr 483	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sscon34b  4251  preqsnd  4811  f1o00  6831  fompt  7088  fcoconst  7105  nvocnv  7254  ordsson  7755  offsplitfpar  8086  funsssuppss  8158  tposf12  8219  suppssfifsupp  9316  cardmin2  9947  acacni  10087  fnct  10484  hash7g  14489  relexpindlem  15066  reccn2  15600  coprmproddvdslem  16672  hashbccl  17015  cshwsdisj  17110  clatlem  18510  dfgrp3lem  19056  ressmulgnn0  19095  mulgnngsum  19097  grpissubg  19164  isnzr2hash  20541  cnfldfunALT  21412  submabas  22611  mdetunilem9  22653  smadiadetlem4  22702  slesolinv  22713  mat2pmatmul  22764  mat2pmatlin  22768  decpmatmul  22805  pm2mpf1  22832  indiscld  23124  cnrest2r  23320  2ndcsb  23482  kgenidm  23580  hausflim  24014  metustfbas  24590  vitalilem1  25643  coseq00topi  26537  coseq0negpitopi  26538  cxplogb  26821  atanlogsublem  26950  cusgredg  29564  dfpth2  29868  usgr2pthlem  29902  wspthnonp  29998  elwwlks2ons3im  30093  usgrwwlks2on  30097  umgrwwlks2on  30098  1to3vfriendship  30422  wlkl0  30508  ssmd2  32454  mdslmd1lem2  32468  difeq  32659  1stpreimas  32851  fpwrelmapffs  32879  insiga  34388  eulerpartlemt  34622  signsvtn0  34821  signlem0  34838  bnj927  35022  derangenlem  35469  bccolsum  36037  cntotbnd  38243  dfac21  43591  tfsconcatrev  43873  eliin2f  45630  wessf1ornlem  45711  founiiun0  45716  disjinfi  45718  pimxrneun  46010  islptre  46143  climlimsupcex  46291  wallispi2lem2  46594  stirlinglem12  46607  fourierdlem12  46641  fourierswlem  46752  qndenserrnbllem  46816  dfsalgen2  46863  sge0ltfirp  46922  sge0resplit  46928  hoidmvlelem1  47117  hoidmvlelem3  47119  hoidmvlelem5  47121  hspdifhsp  47138  fresfo  47590  uniimaprimaeqfv  47936  usgrgrtrirex  48520  uspgrlimlem3  48560  grlimedgclnbgr  48565  gpg5gricstgr3  48660  gpgprismgr4cycllem8  48672  lincfsuppcl  48983  lincvalpr  48988  ldepsnlinclem1  49075  ldepsnlinclem2  49076  nn0sumshdiglemB  49190  euendfunc2  50096  incat  50170