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  4256  preqsnd  4823  f1o00  6856  fompt  7113  fcoconst  7130  nvocnv  7279  ordsson  7781  offsplitfpar  8113  funsssuppss  8185  tposf12  8246  suppssfifsupp  9339  cardmin2  9984  acacni  10123  fnct  10520  hash7g  14523  relexpindlem  15100  reccn2  15648  coprmproddvdslem  16719  hashbccl  17062  cshwsdisj  17157  clatlem  18557  dfgrp3lem  19103  ressmulgnn0  19142  mulgnngsum  19144  grpissubg  19212  isnzr2hash  20602  cnfldfunALT  21516  submabas  22714  mdetunilem9  22756  smadiadetlem4  22805  slesolinv  22816  mat2pmatmul  22867  mat2pmatlin  22871  decpmatmul  22908  pm2mpf1  22935  indiscld  23227  cnrest2r  23423  2ndcsb  23585  kgenidm  23683  hausflim  24117  metustfbas  24693  vitalilem1  25746  coseq00topi  26643  coseq0negpitopi  26644  cxplogb  26927  atanlogsublem  27056  cusgredg  29740  dfpth2  30044  usgr2pthlem  30078  wspthnonp  30174  elwwlks2ons3im  30269  usgrwwlks2on  30273  umgrwwlks2on  30274  1to3vfriendship  30598  wlkl0  30684  ssmd2  32630  mdslmd1lem2  32644  difeq  32830  1stpreimas  33017  fpwrelmapffs  33045  insiga  34493  eulerpartlemt  34727  signsvtn0  34923  signlem0  34940  bnj927  35124  ordprcon  35444  derangenlem  35629  bccolsum  36197  cntotbnd  38413  dfac21  43763  tfsconcatrev  44045  eliin2f  45792  wessf1ornlem  45873  founiiun0  45878  disjinfi  45880  pimxrneun  46172  islptre  46305  climlimsupcex  46453  wallispi2lem2  46756  stirlinglem12  46769  fourierdlem12  46803  fourierswlem  46914  qndenserrnbllem  46978  dfsalgen2  47025  sge0ltfirp  47084  sge0resplit  47090  hoidmvlelem1  47279  hoidmvlelem3  47281  hoidmvlelem5  47283  hspdifhsp  47300  fresfo  47752  uniimaprimaeqfv  48098  usgrgrtrirex  48682  uspgrlimlem3  48722  grlimedgclnbgr  48727  gpg5gricstgr3  48822  gpgprismgr4cycllem8  48834  lincfsuppcl  49160  lincvalpr  49165  ldepsnlinclem1  49252  ldepsnlinclem2  49253  nn0sumshdiglemB  49367  euendfunc2  50272  incat  50346