Theorem bilani 510

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

Proof of Theorem bilani

Step	Hyp	Ref	Expression
1		birani.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 219	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantl 487	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:  gencbvex  3510  sscon34b  4252  propeqop  5483  elrelb  5780  iotanul2  6529  fimacnvinrn2  7096  riota2df  7423  riotaxfrd  7434  fprresex  8356  erinxp  8840  resixp  8989  unxpdomlem3  9277  unfilem1  9325  fsuppunbi  9408  mapfien  9427  marypha1lem  9452  marypha2lem3  9456  suplub  9479  brwdom3  9603  ttrclselem2  9754  r1tr  9810  harcard  10086  acnnum  10158  dfacacn  10247  dfac12lem3  10251  kmlem4  10259  infpss  10321  ackbij1lem12  10335  fin23lem41  10457  fin1a2lem11  10515  fpwwe2lem12  10754  pwfseq  10776  intwun  10847  inttsk  10886  intgru  10926  indval2  12352  xov1plusxeqvd  13656  tpf1o  14673  swrdnznd  14818  pfxccat3  14911  relexpsucnnr  15207  lo1eq  15764  rlimeq  15765  iserex  15853  fsum2dlem  15965  fsumcom2  15969  bcxmas  16033  fprod2dlem  16176  fprodcom2  16180  risefacp1  16224  fallfacp1  16225  rpnnen2lem10  16420  bezoutlem3  16743  eucalgf  16787  prmind2  16889  prmgaplem7  17264  ressabs  17455  mrcuni  17824  mreexmrid  17846  mreexexlem4d  17850  chnso  18827  smndex2dnrinv  19143  dfgrp2  19202  lagsubg  19439  cycsubmcom  19448  gastacl  19553  orbsta2  19558  idrespermg  19655  psgnunilem4  19741  sylow2alem1  19861  efgrelexlemb  19994  unitgrp  20643  unitnegcl  20657  elrhmunit  20790  subrguss  20869  issubdrg  21067  lspsncv0  21454  rspvalint  21553  frlmbas3  22112  lindsenlbs  22187  psrbagconcl  22265  rhmpsrlem2  22279  psrlidm  22299  psrridm  22300  psrass1  22301  psrcom  22305  mvrcl  22329  mplcoe1  22376  cply1mul  22644  matvscacell  22781  scmatscm  22858  smatvscl  22869  m2detleib  22976  gsummatr01lem3  23002  slesolex  23030  cramerimplem2  23032  ntrdif  23400  clsdif  23401  isclo  23435  neiptoptop  23479  resttopon  23509  cmpfi  23756  conncompconn  23780  2ndcctbss  23804  dis2ndc  23809  dislly  23846  lfinun  23874  dissnref  23877  qtopid  24054  qtopcmplem  24056  trfil1  24235  tgpmulg  24442  utoptop  24583  ucnima  24629  setsmstopn  24827  metustfbas  24906  cfilucfil  24908  tngtopn  24999  bndth  25309  pi1blem  25390  bcth  25680  ovolicc2lem2  25869  ovolicc2  25873  vitalilem1  25959  vitalilem2  25960  vitalilem3  25961  itg2split  26100  ditgsplitlem  26210  limccnp2  26242  dvexp3  26328  radcnv0  26773  abelth2  26799  pilem3  26810  eff1olem  26906  dvloglem  27006  logtayl  27018  asinsinlem  27249  atans2  27289  ppisval2  27462  isppw  27471  chtppilimlem2  27831  chebbnd2  27834  abvcxp  27972  noinfbnd2lem1  28117  legov2  29079  colopp  29277  dfcgra2  29368  cgraer  29407  cgrabasimass  29408  angmgmlem  29425  prlngsym  29449  usgr1v0e  29937  dfnbgr3  29949  nbusgrf1o0  29980  nb3gr2nb  29995  usgr2pthlem  30379  crctcshwlkn0  30440  wspthnp  30469  2wlkdlem6  30550  elwwlks2ons3im  30573  usgrwwlks2on  30577  umgrwwlks2on  30578  clwwlknclwwlkdifnum  30601  clwwlkf  30668  clwwlknonex2  30730  eupthp1  30847  frgrncvvdeqlem3  30932  ubthlem3  31504  htth  31550  mdslmd4i  32965  mdsymlem3  33037  acunirnmpt  33325  aciunf1lem  33328  aciunf1  33329  suppovss  33345  hashxpe  33469  fsumiunle  33490  xrsmulgzz  33640  gsummpt2co  33679  gsumwrd2dccatlem  33708  cycpmgcl  33784  archiabl  33829  isarchiofld  33830  elrgspnlem4  33876  elrgspnsubrunlem1  33878  fldgensdrg  33946  kerunit  33956  nsgqusf1olem1  34034  nsgqusf1olem3  34036  elrspunidl  34048  dflring3  34099  dflring4  34100  rprmirredb  34134  1arithidom  34139  1arithufdlem4  34149  0ringmon1p  34159  selvply1rhmlem2  34223  mplvrpmmhm  34248  esplyfval3  34274  vieta  34282  lindsun  34327  fedgmul  34333  irngnzply1  34393  lmat22lem  34519  reff  34541  locfinreflem  34542  zarclsiin  34573  pstmfval  34598  rge0scvg  34651  gsumesum  34761  esumrnmpt2  34770  esumfzf  34771  hasheuni  34787  esumcvgsum  34790  esumgect  34792  esum2dlem  34794  esum2d  34795  esumiun  34796  ispisys2  34856  sigapisys  34858  unelldsys  34861  sigapildsys  34865  voliune  34932  oms0  34999  eulerpartlems  35062  eulerpartlemt  35073  actfunsnf1o  35303  actfunsnrndisj  35304  breprexplema  35329  bnj1388  35733  bnj1408  35736  soinfdom  35800  fineqvnttrclse  35892  gdlopcfv1  35972  gdlopcfv2  35973  gdlopcfv3  35974  gdlopcfv4  35975  gdlopcfv5  35976  gdlopcfv6  35977  gdlopcfv7  35978  j0ltalephlem  36007  k3n0j0lt  36020  jltaleph  36026  subfacp1lem3  36114  subfacp1lem5  36116  satffunlem2lem2  36338  elmsta  36480  faclim  36689  fnessref  37323  bj-prmoore  38227  lindsadd  38728  poimirlem25  38755  mbfresfi  38776  ftc1anclem6  38808  lkr0f  40343  2polssN  41164  aks4d1p7  43325  primrootspoweq0  43348  aks6d1c4  43366  hashnexinjle  43371  sticksstones1  43388  sticksstones2  43389  sticksstones3  43390  sticksstones10  43397  sticksstones12  43400  aks6d1c6lem3  43414  aks6d1c6isolem1  43416  aks6d1c6isolem2  43417  aks6d1c7  43426  rhmqusspan  43427  grpods  43436  unitscyglem1  43437  unitscyglem2  43438  unitscyglem3  43439  unitscyglem4  43440  unitscyglem5  43441  dford3lem1  44226  dfac21  44261  oninfex2  44439  clsk1indlem3  45235  ntrclsiso  45259  ntrclsk3  45262  ntrclsk13  45263  imo72b2  45364  bcc0  45516  iunincfi  46314  restuni3  46338  suprnmpt  46394  wessf1ornlem  46405  disjf1o  46411  choicefi  46419  mapssbi  46431  unirnmapsn  46432  infnsuprnmpt  46467  fzisoeu  46521  upbdrech  46526  iuneqfzuzlem  46551  supxrleubrnmpt  46621  suprleubrnmpt  46637  infrnmptle  46638  uzub  46646  infxrgelbrnmpt  46669  fprodcn  46817  climsuselem1  46824  climsuse  46825  climeldmeq  46880  climfveq  46884  climfveqf  46895  limsupresico  46915  limsupvaluz  46923  limsupubuz  46928  liminfresico  46986  liminfvalxr  46998  climresdm  47065  xlimresdm  47074  cncfioobdlem  47111  dvbdfbdioo  47145  dvnprodlem2  47162  stoweidlem52  47267  stirlinglem7  47295  stirlinglem10  47298  stirlinglem13  47301  fourierdlem20  47342  fourierdlem25  47347  fourierdlem33  47355  fourierdlem42  47364  fourierdlem57  47378  fourierdlem58  47379  fourierdlem59  47380  fourierdlem65  47386  fourierdlem68  47389  fourierdlem70  47391  fourierdlem71  47392  fourierdlem74  47395  fourierdlem75  47396  fourierdlem80  47401  fourierdlem101  47422  ioorrnopn  47520  ioorrnopnxr  47522  subsaliuncl  47573  sge0rnbnd  47608  sge0lefi  47613  sge0resplit  47621  sge0split  47624  sge0iunmptlemfi  47628  sge0fodjrnlem  47631  sge0iunmpt  47633  sge0isum  47642  sge0xp  47644  sge0seq  47661  sge0reuz  47662  sge0reuzb  47663  ismeannd  47682  psmeasure  47686  meaiuninclem  47695  hoidmv1lelem1  47806  hoidmv1le  47809  hoidmvlelem1  47810  hoidmvle  47815  hoiqssbllem2  47838  opnvonmbllem2  47848  ovolval4lem2  47865  iinhoiicc  47889  vonioo  47897  vonicc  47900  smfaddlem1  47978  smflimlem6  47991  nsssmfmbf  47994  smfresal  48003  smfpimcc  48023  smflimsupmpt  48044  smfliminfmpt  48047  chnerlem1  48097  sqrtnzqaa  48119  cfsetsnfsetf  48333  euoreqb  48385  fargshiftfo  48729  paireqne  48798  dfclnbgr3  49129  isuspgrim0lem  49196  isuspgrimlem  49198  usgrgrtrirex  49253  grlimprclnbgrvtx  49302  gpgprismgr4cycllem8  49405  lcoop  49728  lincvalsc0  49738  linc0scn0  49740  snlindsntor  49788  rege1logbrege0  49875  prelrrx2bd  50031  dmrnxp  50153  mofsn2  50161