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  4253  preqsnd  4822  f1o00  6857  fompt  7114  fcoconst  7131  nvocnv  7285  ordsson  7785  offsplitfpar  8119  funsssuppss  8191  tposf12  8252  suppssfifsupp  9353  cardmin2  10007  acacni  10146  fnct  10547  fnctOLD  10548  hash7g  14553  relexpindlem  15138  reccn2  15686  coprmproddvdslem  16756  hashbccl  17099  cshwsdisj  17194  clatlem  18594  dfgrp3lem  19165  ressmulgnn0  19204  mulgnngsum  19206  grpissubg  19274  isnzr2hash  20684  cnfldfunALT  21604  submabas  22804  mdetunilem9  22846  smadiadetlem4  22895  slesolinv  22909  mat2pmatmul  22960  mat2pmatlin  22964  decpmatmul  23001  pm2mpf1  23028  indiscld  23320  cnrest2r  23516  2ndcsb  23678  kgenidm  23777  hausflim  24211  metustfbas  24787  vitalilem1  25840  coseq00topi  26740  coseq0negpitopi  26741  cxplogb  27024  atanlogsublem  27153  cusgredg  29885  dfpth2  30194  usgr2pthlem  30229  wspthnonp  30328  elwwlks2ons3im  30423  usgrwwlks2on  30427  umgrwwlks2on  30428  1to3vfriendship  30762  wlkl0  30848  ssmd2  32794  mdslmd1lem2  32808  difeq  32994  1stpreimas  33180  fpwrelmapffs  33207  insiga  34650  eulerpartlemt  34884  signsvtn0  35080  signlem0  35097  bnj927  35281  ordprcon  35594  derangenlem  35752  bccolsum  36320  cntotbnd  38548  dfac21  43909  tfsconcatrev  44191  eliin2f  45938  wessf1ornlem  46019  founiiun0  46024  disjinfi  46026  pimxrneun  46318  islptre  46451  climlimsupcex  46599  wallispi2lem2  46902  stirlinglem12  46915  fourierdlem12  46949  fourierswlem  47060  qndenserrnbllem  47124  dfsalgen2  47171  sge0ltfirp  47230  sge0resplit  47236  hoidmvlelem1  47425  hoidmvlelem3  47427  hoidmvlelem5  47429  hspdifhsp  47446  fresfo  47938  uniimaprimaeqfv  48284  usgrgrtrirex  48868  uspgrlimlem3  48908  grlimedgclnbgr  48913  gpg5gricstgr3  49008  gpgprismgr4cycllem8  49020  lincfsuppcl  49345  lincvalpr  49350  ldepsnlinclem1  49437  ldepsnlinclem2  49438  nn0sumshdiglemB  49552  euendfunc2  50455  incat  50529