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  6860  fompt  7118  fcoconst  7135  nvocnv  7289  ordsson  7797  offsplitfpar  8130  funsssuppss  8208  tposf12  8269  suppssfifsupp  9373  cardmin2  10081  acacni  10220  fnct  10621  fnctOLD  10622  hash7g  14632  relexpindlem  15217  reccn2  15765  coprmproddvdslem  16838  hashbccl  17182  cshwsdisj  17277  clatlem  18677  dfgrp3lem  19249  ressmulgnn0  19288  mulgnngsum  19290  grpissubg  19358  isnzr2hash  20771  cnfldfunALT  21694  submabas  22894  mdetunilem9  22936  smadiadetlem4  22985  slesolinv  22999  mat2pmatmul  23050  mat2pmatlin  23054  decpmatmul  23091  pm2mpf1  23118  indiscld  23410  cnrest2r  23606  2ndcsb  23768  kgenidm  23867  hausflim  24301  metustfbas  24877  vitalilem1  25930  coseq00topi  26832  coseq0negpitopi  26833  cxplogb  27115  atanlogsublem  27244  cusgredg  30006  dfpth2  30315  usgr2pthlem  30350  wspthnonp  30449  elwwlks2ons3im  30544  usgrwwlks2on  30548  umgrwwlks2on  30549  1to3vfriendship  30883  wlkl0  30969  ssmd2  32915  mdslmd1lem2  32929  difeq  33157  1stpreimas  33342  fpwrelmapffs  33369  insiga  34813  eulerpartlemt  35046  signsvtn0  35242  signlem0  35259  bnj927  35443  ordprcon  35759  derangenlem  36005  bccolsum  36579  cntotbnd  38806  dfac21  44144  tfsconcatrev  44426  eliin2f  46195  wessf1ornlem  46276  founiiun0  46281  disjinfi  46283  pimxrneun  46574  islptre  46707  climlimsupcex  46855  wallispi2lem2  47158  stirlinglem12  47171  fourierdlem12  47205  fourierswlem  47316  qndenserrnbllem  47380  dfsalgen2  47427  sge0ltfirp  47486  sge0resplit  47492  hoidmvlelem1  47681  hoidmvlelem3  47683  hoidmvlelem5  47685  hspdifhsp  47702  fresfo  48194  uniimaprimaeqfv  48540  usgrgrtrirex  49124  uspgrlimlem3  49164  grlimedgclnbgr  49169  gpg5gricstgr3  49264  gpgprismgr4cycllem8  49276  lincfsuppcl  49601  lincvalpr  49606  ldepsnlinclem1  49693  ldepsnlinclem2  49694  nn0sumshdiglemB  49808  euendfunc2  50711  incat  50785