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  4249  preqsnd  4818  f1o00  6848  fompt  7106  fcoconst  7123  nvocnv  7277  ordsson  7780  offsplitfpar  8113  funsssuppss  8185  tposf12  8246  suppssfifsupp  9350  cardmin2  10052  acacni  10191  fnct  10592  fnctOLD  10593  hash7g  14599  relexpindlem  15184  reccn2  15732  coprmproddvdslem  16800  hashbccl  17143  cshwsdisj  17238  clatlem  18638  dfgrp3lem  19210  ressmulgnn0  19249  mulgnngsum  19251  grpissubg  19319  isnzr2hash  20732  cnfldfunALT  21655  submabas  22855  mdetunilem9  22897  smadiadetlem4  22946  slesolinv  22960  mat2pmatmul  23011  mat2pmatlin  23015  decpmatmul  23052  pm2mpf1  23079  indiscld  23371  cnrest2r  23567  2ndcsb  23729  kgenidm  23828  hausflim  24262  metustfbas  24838  vitalilem1  25891  coseq00topi  26795  coseq0negpitopi  26796  cxplogb  27078  atanlogsublem  27207  cusgredg  29939  dfpth2  30248  usgr2pthlem  30283  wspthnonp  30382  elwwlks2ons3im  30477  usgrwwlks2on  30481  umgrwwlks2on  30482  1to3vfriendship  30816  wlkl0  30902  ssmd2  32848  mdslmd1lem2  32862  difeq  33048  1stpreimas  33233  fpwrelmapffs  33260  insiga  34704  eulerpartlemt  34938  signsvtn0  35134  signlem0  35151  bnj927  35335  ordprcon  35648  derangenlem  35857  bccolsum  36425  cntotbnd  38650  dfac21  44011  tfsconcatrev  44293  eliin2f  46040  wessf1ornlem  46121  founiiun0  46126  disjinfi  46128  pimxrneun  46420  islptre  46553  climlimsupcex  46701  wallispi2lem2  47004  stirlinglem12  47017  fourierdlem12  47051  fourierswlem  47162  qndenserrnbllem  47226  dfsalgen2  47273  sge0ltfirp  47332  sge0resplit  47338  hoidmvlelem1  47527  hoidmvlelem3  47529  hoidmvlelem5  47531  hspdifhsp  47548  fresfo  48040  uniimaprimaeqfv  48386  usgrgrtrirex  48970  uspgrlimlem3  49010  grlimedgclnbgr  49015  gpg5gricstgr3  49110  gpgprismgr4cycllem8  49122  lincfsuppcl  49447  lincvalpr  49452  ldepsnlinclem1  49539  ldepsnlinclem2  49540  nn0sumshdiglemB  49654  euendfunc2  50557  incat  50631