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

Proof of Theorem bilani

Step	Hyp	Ref	Expression
1		birani.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 219	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantl 486	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:  gencbvex  3513  sscon34b  4259  propeqop  5481  iotanul2  6498  fimacnvinrn2  7057  riota2df  7380  riotaxfrd  7391  fprresex  8295  erinxp  8777  resixp  8919  unxpdomlem3  9206  unfilem1  9253  fsuppunbi  9337  mapfien  9356  marypha1lem  9381  marypha2lem3  9385  suplub  9408  brwdom3  9532  ttrclselem2  9683  r1tr  9736  harcard  9952  acnnum  10024  dfacacn  10113  dfac12lem3  10117  kmlem4  10125  infpss  10187  ackbij1lem12  10201  fin23lem41  10324  fin1a2lem11  10382  fpwwe2lem12  10615  pwfseq  10637  intwun  10708  inttsk  10747  intgru  10787  indval2  12214  xov1plusxeqvd  13516  tpf1o  14528  swrdnznd  14670  pfxccat3  14761  relexpsucnnr  15052  lo1eq  15609  rlimeq  15610  iserex  15698  fsum2dlem  15811  fsumcom2  15815  bcxmas  15879  fprod2dlem  16024  fprodcom2  16028  risefacp1  16073  fallfacp1  16074  rpnnen2lem10  16269  bezoutlem3  16589  eucalgf  16631  prmind2  16733  prmgaplem7  17107  ressabs  17298  mrcuni  17667  mreexmrid  17689  mreexexlem4d  17693  chnso  18670  smndex2dnrinv  18967  dfgrp2  19019  lagsubg  19257  cycsubmcom  19266  gastacl  19370  orbsta2  19375  idrespermg  19472  psgnunilem4  19558  sylow2alem1  19678  efgrelexlemb  19811  unitgrp  20456  unitnegcl  20470  elrhmunit  20584  subrguss  20663  issubdrg  20852  lspsncv0  21239  frlmbas3  21886  psrbagconcl  22037  rhmpsrlem2  22051  psrlidm  22071  psrridm  22072  psrass1  22073  psrcom  22077  mvrcl  22101  mplcoe1  22148  cply1mul  22417  matvscacell  22554  scmatscm  22631  smatvscl  22642  m2detleib  22749  gsummatr01lem3  22775  slesolex  22800  cramerimplem2  22802  ntrdif  23170  clsdif  23171  isclo  23205  neiptoptop  23249  resttopon  23279  cmpfi  23526  conncompconn  23550  2ndcctbss  23573  dis2ndc  23578  dislly  23615  lfinun  23643  dissnref  23646  qtopid  23823  qtopcmplem  23825  trfil1  24004  tgpmulg  24211  utoptop  24352  ucnima  24398  setsmstopn  24596  metustfbas  24675  cfilucfil  24677  tngtopn  24768  bndth  25078  pi1blem  25159  bcth  25449  ovolicc2lem2  25638  ovolicc2  25642  vitalilem1  25728  vitalilem2  25729  vitalilem3  25730  itg2split  25869  ditgsplitlem  25980  limccnp2  26012  dvexp3  26098  radcnv0  26537  abelth2  26563  pilem3  26574  eff1olem  26671  dvloglem  26771  logtayl  26783  asinsinlem  27014  atans2  27054  ppisval2  27227  isppw  27236  chtppilimlem2  27596  chebbnd2  27599  abvcxp  27737  noinfbnd2lem1  27852  legov2  28813  colopp  29000  dfcgra2  29082  prlngsym  29126  usgr1v0e  29585  dfnbgr3  29597  nbusgrf1o0  29628  nb3gr2nb  29643  usgr2pthlem  30021  crctcshwlkn0  30079  wspthnp  30108  2wlkdlem6  30189  elwwlks2ons3im  30212  usgrwwlks2on  30216  umgrwwlks2on  30217  clwwlknclwwlkdifnum  30240  clwwlkf  30307  clwwlknonex2  30369  eupthp1  30476  frgrncvvdeqlem3  30561  ubthlem3  31133  htth  31179  mdslmd4i  32594  mdsymlem3  32666  acunirnmpt  32916  aciunf1lem  32919  aciunf1  32920  suppovss  32938  hashxpe  33064  fsumiunle  33086  xrsmulgzz  33242  gsummpt2co  33281  gsumwrd2dccatlem  33310  cycpmgcl  33386  archiabl  33431  isarchiofld  33432  elrgspnlem4  33478  elrgspnsubrunlem1  33480  fldgensdrg  33550  kerunit  33560  nsgqusf1olem1  33638  nsgqusf1olem3  33640  elrspunidl  33652  dflring3  33704  dflring4  33705  rprmirredb  33739  1arithidom  33744  1arithufdlem4  33754  0ringmon1p  33764  mplvrpmga  33852  mplvrpmmhm  33853  esplyfval3  33879  vieta  33887  lindsun  33932  fedgmul  33938  irngnzply1  33998  lmat22lem  34124  reff  34146  locfinreflem  34147  zarclsiin  34178  pstmfval  34203  rge0scvg  34256  gsumesum  34366  esumrnmpt2  34375  esumfzf  34376  hasheuni  34392  esumcvgsum  34395  esumgect  34397  esum2dlem  34399  esum2d  34400  esumiun  34401  ispisys2  34460  sigapisys  34462  unelldsys  34465  sigapildsys  34469  voliune  34536  oms0  34604  eulerpartlems  34667  eulerpartlemt  34678  actfunsnf1o  34908  actfunsnrndisj  34909  breprexplema  34934  bnj1388  35338  bnj1408  35341  fineqvnttrclse  35432  subfacp1lem3  35545  subfacp1lem5  35547  satffunlem2lem2  35769  elmsta  35911  faclim  36109  fnessref  36730  bj-prmoore  37617  lindsadd  38124  lindsenlbs  38126  poimirlem25  38156  mbfresfi  38177  ftc1anclem6  38209  lkr0f  39730  2polssN  40551  aks4d1p7  42712  primrootspoweq0  42735  aks6d1c4  42753  hashnexinjle  42758  sticksstones1  42775  sticksstones2  42776  sticksstones3  42777  sticksstones10  42784  sticksstones12  42787  aks6d1c6lem3  42801  aks6d1c6isolem1  42803  aks6d1c6isolem2  42804  aks6d1c7  42813  rhmqusspan  42814  grpods  42823  unitscyglem1  42824  unitscyglem2  42825  unitscyglem3  42826  unitscyglem4  42827  unitscyglem5  42828  dford3lem1  43615  dfac21  43655  oninfex2  43834  clsk1indlem3  44631  ntrclsiso  44655  ntrclsk3  44658  ntrclsk13  44659  imo72b2  44760  bcc0  44914  iunincfi  45670  restuni3  45694  suprnmpt  45750  wessf1ornlem  45761  disjf1o  45767  choicefi  45775  mapssbi  45787  unirnmapsn  45788  infnsuprnmpt  45823  fzisoeu  45877  upbdrech  45882  iuneqfzuzlem  45908  supxrleubrnmpt  45978  suprleubrnmpt  45994  infrnmptle  45995  uzub  46003  infxrgelbrnmpt  46026  fprodcn  46174  climsuselem1  46181  climsuse  46182  climeldmeq  46237  climfveq  46241  climfveqf  46252  limsupresico  46272  limsupvaluz  46280  limsupubuz  46285  liminfresico  46343  liminfvalxr  46355  climresdm  46422  xlimresdm  46431  cncfioobdlem  46468  dvbdfbdioo  46502  dvnprodlem2  46519  stoweidlem52  46624  stirlinglem7  46652  stirlinglem10  46655  stirlinglem13  46658  fourierdlem20  46699  fourierdlem25  46704  fourierdlem33  46712  fourierdlem42  46721  fourierdlem57  46735  fourierdlem58  46736  fourierdlem59  46737  fourierdlem65  46743  fourierdlem68  46746  fourierdlem70  46748  fourierdlem71  46749  fourierdlem74  46752  fourierdlem75  46753  fourierdlem80  46758  fourierdlem101  46779  ioorrnopn  46877  ioorrnopnxr  46879  subsaliuncl  46930  sge0rnbnd  46965  sge0lefi  46970  sge0resplit  46978  sge0split  46981  sge0iunmptlemfi  46985  sge0fodjrnlem  46988  sge0iunmpt  46990  sge0isum  46999  sge0xp  47001  sge0seq  47018  sge0reuz  47019  sge0reuzb  47020  ismeannd  47039  psmeasure  47043  meaiuninclem  47052  hoidmv1lelem1  47163  hoidmv1le  47166  hoidmvlelem1  47167  hoidmvle  47172  hoiqssbllem2  47195  opnvonmbllem2  47205  ovolval4lem2  47222  iinhoiicc  47246  vonioo  47254  vonicc  47257  smfaddlem1  47335  smflimlem6  47348  nsssmfmbf  47351  smfresal  47360  smfpimcc  47380  smflimsupmpt  47401  smfliminfmpt  47404  chnerlem1  47456  cfsetsnfsetf  47650  euoreqb  47701  fargshiftfo  48046  paireqne  48115  dfclnbgr3  48446  isuspgrim0lem  48513  isuspgrimlem  48515  usgrgrtrirex  48570  grlimprclnbgrvtx  48619  gpgprismgr4cycllem8  48722  lcoop  49042  lincvalsc0  49052  linc0scn0  49054  snlindsntor  49102  rege1logbrege0  49189  dmrnxp  49466  mofsn2  49474