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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

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 401

This theorem is used by:  sscon34b  4256  preqsnd  4823  f1o00  6856  fompt  7113  fcoconst  7130  nvocnv  7279  ordsson  7780  offsplitfpar  8112  funsssuppss  8184  tposf12  8245  suppssfifsupp  9338  cardmin2  9992  acacni  10131  fnct  10527  hash7g  14530  relexpindlem  15107  reccn2  15655  coprmproddvdslem  16726  hashbccl  17069  cshwsdisj  17164  clatlem  18564  dfgrp3lem  19110  ressmulgnn0  19149  mulgnngsum  19151  grpissubg  19219  isnzr2hash  20628  cnfldfunALT  21548  submabas  22746  mdetunilem9  22788  smadiadetlem4  22837  slesolinv  22848  mat2pmatmul  22899  mat2pmatlin  22903  decpmatmul  22940  pm2mpf1  22967  indiscld  23259  cnrest2r  23455  2ndcsb  23617  kgenidm  23715  hausflim  24149  metustfbas  24725  vitalilem1  25778  coseq00topi  26678  coseq0negpitopi  26679  cxplogb  26962  atanlogsublem  27091  cusgredg  29785  dfpth2  30089  usgr2pthlem  30123  wspthnonp  30219  elwwlks2ons3im  30314  usgrwwlks2on  30318  umgrwwlks2on  30319  1to3vfriendship  30643  wlkl0  30729  ssmd2  32675  mdslmd1lem2  32689  difeq  32875  1stpreimas  33062  fpwrelmapffs  33090  insiga  34536  eulerpartlemt  34770  signsvtn0  34966  signlem0  34983  bnj927  35167  ordprcon  35487  derangenlem  35671  bccolsum  36239  cntotbnd  38475  dfac21  43821  tfsconcatrev  44103  eliin2f  45850  wessf1ornlem  45931  founiiun0  45936  disjinfi  45938  pimxrneun  46230  islptre  46363  climlimsupcex  46511  wallispi2lem2  46814  stirlinglem12  46827  fourierdlem12  46861  fourierswlem  46972  qndenserrnbllem  47036  dfsalgen2  47083  sge0ltfirp  47142  sge0resplit  47148  hoidmvlelem1  47337  hoidmvlelem3  47339  hoidmvlelem5  47341  hspdifhsp  47358  fresfo  47813  uniimaprimaeqfv  48159  usgrgrtrirex  48743  uspgrlimlem3  48783  grlimedgclnbgr  48788  gpg5gricstgr3  48883  gpgprismgr4cycllem8  48895  lincfsuppcl  49221  lincvalpr  49226  ldepsnlinclem1  49313  ldepsnlinclem2  49314  nn0sumshdiglemB  49428  euendfunc2  50333  incat  50407