Theorem bilani 507

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 218	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantl 484	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  gencbvex  3504  sscon34b  4251  propeqop  5470  iotanul2  6483  fimacnvinrn2  7042  riota2df  7365  riotaxfrd  7376  fprresex  8279  erinxp  8761  resixp  8904  unxpdomlem3  9191  unfilem1  9238  fsuppunbi  9325  mapfien  9344  marypha1lem  9369  marypha2lem3  9373  suplub  9396  brwdom3  9520  ttrclselem2  9671  r1tr  9724  harcard  9926  acnnum  9998  dfacacn  10088  dfac12lem3  10092  kmlem4  10100  infpss  10162  ackbij1lem12  10176  fin23lem41  10299  fin1a2lem11  10357  fpwwe2lem12  10590  pwfseq  10612  intwun  10683  inttsk  10722  intgru  10762  indval2  12190  xov1plusxeqvd  13492  tpf1o  14504  swrdnznd  14646  pfxccat3  14737  relexpsucnnr  15028  lo1eq  15571  rlimeq  15572  iserex  15660  fsum2dlem  15773  fsumcom2  15777  bcxmas  15841  fprod2dlem  15986  fprodcom2  15990  risefacp1  16035  fallfacp1  16036  rpnnen2lem10  16231  bezoutlem3  16551  eucalgf  16593  prmind2  16695  prmgaplem7  17069  ressabs  17260  mrcuni  17629  mreexmrid  17651  mreexexlem4d  17655  chnso  18632  smndex2dnrinv  18928  dfgrp2  18980  lagsubg  19212  cycsubmcom  19221  gastacl  19325  orbsta2  19330  idrespermg  19427  psgnunilem4  19513  sylow2alem1  19633  efgrelexlemb  19766  unitgrp  20404  unitnegcl  20418  elrhmunit  20532  subrguss  20609  issubdrg  20802  lspsncv0  21189  frlmbas3  21801  psrbagconcl  21952  rhmpsrlem2  21966  psrlidm  21986  psrridm  21987  psrass1  21988  psrcom  21992  mvrcl  22016  mplcoe1  22063  cply1mul  22332  matvscacell  22469  scmatscm  22546  smatvscl  22557  m2detleib  22664  gsummatr01lem3  22690  slesolex  22715  cramerimplem2  22717  ntrdif  23085  clsdif  23086  isclo  23120  neiptoptop  23164  resttopon  23194  cmpfi  23441  conncompconn  23465  2ndcctbss  23488  dis2ndc  23493  dislly  23530  lfinun  23558  dissnref  23561  qtopid  23738  qtopcmplem  23740  trfil1  23919  tgpmulg  24126  utoptop  24267  ucnima  24313  setsmstopn  24511  metustfbas  24590  cfilucfil  24592  tngtopn  24683  bndth  24993  pi1blem  25074  bcth  25364  ovolicc2lem2  25553  ovolicc2  25557  vitalilem1  25643  vitalilem2  25644  vitalilem3  25645  itg2split  25784  ditgsplitlem  25895  limccnp2  25927  dvexp3  26013  radcnv0  26449  abelth2  26475  pilem3  26486  eff1olem  26583  dvloglem  26683  logtayl  26695  asinsinlem  26926  atans2  26966  ppisval2  27139  isppw  27148  chtppilimlem2  27508  chebbnd2  27511  abvcxp  27649  noinfbnd2lem1  27764  legov2  28725  colopp  28908  dfcgra2  28969  usgr1v0e  29466  dfnbgr3  29478  nbusgrf1o0  29509  nb3gr2nb  29524  usgr2pthlem  29902  crctcshwlkn0  29960  wspthnp  29989  2wlkdlem6  30070  elwwlks2ons3im  30093  usgrwwlks2on  30097  umgrwwlks2on  30098  clwwlknclwwlkdifnum  30121  clwwlkf  30188  clwwlknonex2  30250  eupthp1  30357  frgrncvvdeqlem3  30442  ubthlem3  31014  htth  31060  mdslmd4i  32475  mdsymlem3  32547  acunirnmpt  32804  aciunf1lem  32807  aciunf1  32808  suppovss  32826  hashxpe  32952  fsumiunle  32974  xrsmulgzz  33141  gsummpt2co  33182  gsumwrd2dccatlem  33211  cycpmgcl  33287  archiabl  33332  isarchiofld  33333  elrgspnlem4  33380  elrgspnsubrunlem1  33382  fldgensdrg  33455  kerunit  33465  nsgqusf1olem1  33553  nsgqusf1olem3  33555  elrspunidl  33568  dflring3  33647  dflring4  33648  rprmirredb  33682  1arithidom  33687  1arithufdlem4  33697  0ringmon1p  33707  mplvrpmga  33796  mplvrpmmhm  33797  esplyfval3  33823  vieta  33831  lindsun  33876  fedgmul  33882  irngnzply1  33942  lmat22lem  34068  reff  34090  locfinreflem  34091  zarclsiin  34122  pstmfval  34147  rge0scvg  34200  gsumesum  34310  esumrnmpt2  34319  esumfzf  34320  hasheuni  34336  esumcvgsum  34339  esumgect  34341  esum2dlem  34343  esum2d  34344  esumiun  34345  ispisys2  34404  sigapisys  34406  unelldsys  34409  sigapildsys  34413  voliune  34480  oms0  34548  eulerpartlems  34611  eulerpartlemt  34622  actfunsnf1o  34855  actfunsnrndisj  34856  breprexplema  34881  bnj1388  35285  bnj1408  35288  fineqvnttrclse  35375  subfacp1lem3  35480  subfacp1lem5  35482  satffunlem2lem2  35704  elmsta  35846  faclim  36044  fnessref  36665  bj-prmoore  37553  lindsadd  38060  lindsenlbs  38062  poimirlem25  38092  mbfresfi  38113  ftc1anclem6  38145  lkr0f  39666  2polssN  40487  aks4d1p7  42648  primrootspoweq0  42671  aks6d1c4  42689  hashnexinjle  42694  sticksstones1  42711  sticksstones2  42712  sticksstones3  42713  sticksstones10  42720  sticksstones12  42723  aks6d1c6lem3  42737  aks6d1c6isolem1  42739  aks6d1c6isolem2  42740  aks6d1c7  42749  rhmqusspan  42750  grpods  42759  unitscyglem1  42760  unitscyglem2  42761  unitscyglem3  42762  unitscyglem4  42763  unitscyglem5  42764  dford3lem1  43551  dfac21  43591  oninfex2  43770  clsk1indlem3  44567  ntrclsiso  44591  ntrclsk3  44594  ntrclsk13  44595  imo72b2  44696  bcc0  44864  iunincfi  45620  restuni3  45644  suprnmpt  45700  wessf1ornlem  45711  disjf1o  45717  choicefi  45725  mapssbi  45737  unirnmapsn  45738  infnsuprnmpt  45773  fzisoeu  45827  upbdrech  45832  iuneqfzuzlem  45858  supxrleubrnmpt  45928  suprleubrnmpt  45944  infrnmptle  45945  uzub  45953  infxrgelbrnmpt  45976  fprodcn  46124  climsuselem1  46131  climsuse  46132  climeldmeq  46187  climfveq  46191  climfveqf  46202  limsupresico  46222  limsupvaluz  46230  limsupubuz  46235  liminfresico  46293  liminfvalxr  46305  climresdm  46372  xlimresdm  46381  cncfioobdlem  46418  dvbdfbdioo  46452  dvnprodlem2  46469  stoweidlem52  46574  stirlinglem7  46602  stirlinglem10  46605  stirlinglem13  46608  fourierdlem20  46649  fourierdlem25  46654  fourierdlem33  46662  fourierdlem42  46671  fourierdlem57  46685  fourierdlem58  46686  fourierdlem59  46687  fourierdlem65  46693  fourierdlem68  46696  fourierdlem70  46698  fourierdlem71  46699  fourierdlem74  46702  fourierdlem75  46703  fourierdlem80  46708  fourierdlem101  46729  ioorrnopn  46827  ioorrnopnxr  46829  subsaliuncl  46880  sge0rnbnd  46915  sge0lefi  46920  sge0resplit  46928  sge0split  46931  sge0iunmptlemfi  46935  sge0fodjrnlem  46938  sge0iunmpt  46940  sge0isum  46949  sge0xp  46951  sge0seq  46968  sge0reuz  46969  sge0reuzb  46970  ismeannd  46989  psmeasure  46993  meaiuninclem  47002  hoidmv1lelem1  47113  hoidmv1le  47116  hoidmvlelem1  47117  hoidmvle  47122  hoiqssbllem2  47145  opnvonmbllem2  47155  ovolval4lem2  47172  iinhoiicc  47196  vonioo  47204  vonicc  47207  smfaddlem1  47285  smflimlem6  47298  nsssmfmbf  47301  smfresal  47310  smfpimcc  47330  smflimsupmpt  47351  smfliminfmpt  47354  chnerlem1  47406  cfsetsnfsetf  47600  euoreqb  47651  fargshiftfo  47996  paireqne  48065  dfclnbgr3  48396  isuspgrim0lem  48463  isuspgrimlem  48465  usgrgrtrirex  48520  grlimprclnbgrvtx  48569  gpgprismgr4cycllem8  48672  lcoop  48981  lincvalsc0  48991  linc0scn0  48993  snlindsntor  49041  rege1logbrege0  49128  dmrnxp  49406  mofsn2  49414