Theorem bilani 505

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  gencbvex  3488  sscon34b  4232  propeqop  5448  iotanul2  6458  fimacnvinrn2  7013  riota2df  7336  riotaxfrd  7347  fprresex  8250  erinxp  8728  resixp  8871  unxpdomlem3  9158  unfilem1  9205  fsuppunbi  9292  mapfien  9311  marypha1lem  9336  marypha2lem3  9340  suplub  9363  brwdom3  9487  ttrclselem2  9638  r1tr  9691  harcard  9893  acnnum  9965  dfacacn  10055  dfac12lem3  10059  kmlem4  10067  infpss  10129  ackbij1lem12  10143  fin23lem41  10265  fin1a2lem11  10323  fpwwe2lem12  10556  pwfseq  10578  intwun  10649  inttsk  10688  intgru  10728  indval2  12155  xov1plusxeqvd  13442  tpf1o  14454  swrdnznd  14596  pfxccat3  14687  relexpsucnnr  14978  lo1eq  15521  rlimeq  15522  iserex  15610  fsum2dlem  15723  fsumcom2  15727  bcxmas  15791  fprod2dlem  15936  fprodcom2  15940  risefacp1  15985  fallfacp1  15986  rpnnen2lem10  16181  bezoutlem3  16501  eucalgf  16543  prmind2  16645  prmgaplem7  17019  ressabs  17209  mrcuni  17578  mreexmrid  17600  mreexexlem4d  17604  chnso  18581  smndex2dnrinv  18877  dfgrp2  18929  lagsubg  19161  cycsubmcom  19170  gastacl  19275  orbsta2  19280  idrespermg  19377  psgnunilem4  19463  sylow2alem1  19583  efgrelexlemb  19716  unitgrp  20354  unitnegcl  20368  elrhmunit  20482  subrguss  20559  issubdrg  20752  lspsncv0  21139  frlmbas3  21751  psrbagconcl  21902  rhmpsrlem2  21916  psrlidm  21936  psrridm  21937  psrass1  21938  psrcom  21942  mvrcl  21966  mplcoe1  22013  cply1mul  22282  matvscacell  22419  scmatscm  22496  smatvscl  22507  m2detleib  22614  gsummatr01lem3  22640  slesolex  22665  cramerimplem2  22667  ntrdif  23035  clsdif  23036  isclo  23070  neiptoptop  23114  resttopon  23144  cmpfi  23391  conncompconn  23415  2ndcctbss  23438  dis2ndc  23443  dislly  23480  lfinun  23508  dissnref  23511  qtopid  23688  qtopcmplem  23690  trfil1  23869  tgpmulg  24076  utoptop  24217  ucnima  24263  setsmstopn  24461  metustfbas  24540  cfilucfil  24542  tngtopn  24633  bndth  24943  pi1blem  25024  bcth  25314  ovolicc2lem2  25503  ovolicc2  25507  vitalilem1  25593  vitalilem2  25594  vitalilem3  25595  itg2split  25734  ditgsplitlem  25845  limccnp2  25877  dvexp3  25963  radcnv0  26399  abelth2  26425  pilem3  26436  eff1olem  26530  dvloglem  26630  logtayl  26642  asinsinlem  26873  atans2  26913  ppisval2  27086  isppw  27095  chtppilimlem2  27455  chebbnd2  27458  abvcxp  27596  noinfbnd2lem1  27712  legov2  28672  colopp  28855  dfcgra2  28916  usgr1v0e  29413  dfnbgr3  29425  nbusgrf1o0  29456  nb3gr2nb  29471  usgr2pthlem  29849  crctcshwlkn0  29907  wspthnp  29936  2wlkdlem6  30017  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  clwwlknclwwlkdifnum  30068  clwwlkf  30135  clwwlknonex2  30197  eupthp1  30304  frgrncvvdeqlem3  30389  ubthlem3  30961  htth  31007  mdslmd4i  32422  mdsymlem3  32494  acunirnmpt  32751  aciunf1lem  32754  aciunf1  32755  suppovss  32773  hashxpe  32899  fsumiunle  32921  xrsmulgzz  33088  gsummpt2co  33129  gsumwrd2dccatlem  33158  cycpmgcl  33234  archiabl  33279  isarchiofld  33280  elrgspnlem4  33326  elrgspnsubrunlem1  33328  fldgensdrg  33398  kerunit  33408  nsgqusf1olem1  33496  nsgqusf1olem3  33498  elrspunidl  33511  rprmirredb  33615  1arithidom  33620  1arithufdlem4  33630  0ringmon1p  33640  mplvrpmga  33729  mplvrpmmhm  33730  esplyfval3  33756  vieta  33764  lindsun  33809  fedgmul  33815  irngnzply1  33875  lmat22lem  34001  reff  34023  locfinreflem  34024  zarclsiin  34055  pstmfval  34080  rge0scvg  34133  gsumesum  34243  esumrnmpt2  34252  esumfzf  34253  hasheuni  34269  esumcvgsum  34272  esumgect  34274  esum2dlem  34276  esum2d  34277  esumiun  34278  ispisys2  34337  sigapisys  34339  unelldsys  34342  sigapildsys  34346  voliune  34413  oms0  34481  eulerpartlems  34544  eulerpartlemt  34555  actfunsnf1o  34788  actfunsnrndisj  34789  breprexplema  34814  bnj1388  35215  bnj1408  35218  fineqvnttrclse  35305  subfacp1lem3  35410  subfacp1lem5  35412  satffunlem2lem2  35634  elmsta  35776  faclim  35974  fnessref  36585  bj-prmoore  37473  lindsadd  37980  lindsenlbs  37982  poimirlem25  38012  mbfresfi  38033  ftc1anclem6  38065  lkr0f  39586  2polssN  40407  aks4d1p7  42568  primrootspoweq0  42591  aks6d1c4  42609  hashnexinjle  42614  sticksstones1  42631  sticksstones2  42632  sticksstones3  42633  sticksstones10  42640  sticksstones12  42643  aks6d1c6lem3  42657  aks6d1c6isolem1  42659  aks6d1c6isolem2  42660  aks6d1c7  42669  rhmqusspan  42670  grpods  42679  unitscyglem1  42680  unitscyglem2  42681  unitscyglem3  42682  unitscyglem4  42683  unitscyglem5  42684  dford3lem1  43471  dfac21  43511  oninfex2  43690  clsk1indlem3  44487  ntrclsiso  44511  ntrclsk3  44514  ntrclsk13  44515  imo72b2  44616  bcc0  44784  iunincfi  45541  restuni3  45565  suprnmpt  45621  wessf1ornlem  45632  disjf1o  45638  choicefi  45646  mapssbi  45658  unirnmapsn  45659  infnsuprnmpt  45694  fzisoeu  45748  upbdrech  45753  iuneqfzuzlem  45779  supxrleubrnmpt  45849  suprleubrnmpt  45865  infrnmptle  45866  uzub  45874  infxrgelbrnmpt  45897  fprodcn  46045  climsuselem1  46052  climsuse  46053  climeldmeq  46108  climfveq  46112  climfveqf  46123  limsupresico  46143  limsupvaluz  46151  limsupubuz  46156  liminfresico  46214  liminfvalxr  46226  climresdm  46293  xlimresdm  46302  cncfioobdlem  46339  dvbdfbdioo  46373  dvnprodlem2  46390  stoweidlem52  46495  stirlinglem7  46523  stirlinglem10  46526  stirlinglem13  46529  fourierdlem20  46570  fourierdlem25  46575  fourierdlem33  46583  fourierdlem42  46592  fourierdlem57  46606  fourierdlem58  46607  fourierdlem59  46608  fourierdlem65  46614  fourierdlem68  46617  fourierdlem70  46619  fourierdlem71  46620  fourierdlem74  46623  fourierdlem75  46624  fourierdlem80  46629  fourierdlem101  46650  ioorrnopn  46748  ioorrnopnxr  46750  subsaliuncl  46801  sge0rnbnd  46836  sge0lefi  46841  sge0resplit  46849  sge0split  46852  sge0iunmptlemfi  46856  sge0fodjrnlem  46859  sge0iunmpt  46861  sge0isum  46870  sge0xp  46872  sge0seq  46889  sge0reuz  46890  sge0reuzb  46891  ismeannd  46910  psmeasure  46914  meaiuninclem  46923  hoidmv1lelem1  47034  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvle  47043  hoiqssbllem2  47066  opnvonmbllem2  47076  ovolval4lem2  47093  iinhoiicc  47117  vonioo  47125  vonicc  47128  smfaddlem1  47206  smflimlem6  47219  nsssmfmbf  47222  smfresal  47231  smfpimcc  47251  smflimsupmpt  47272  smfliminfmpt  47275  chnerlem1  47327  cfsetsnfsetf  47521  euoreqb  47572  fargshiftfo  47917  paireqne  47986  dfclnbgr3  48317  isuspgrim0lem  48384  isuspgrimlem  48386  usgrgrtrirex  48441  grlimprclnbgrvtx  48490  gpgprismgr4cycllem8  48593  lcoop  48902  lincvalsc0  48912  linc0scn0  48914  snlindsntor  48962  rege1logbrege0  49049  dmrnxp  49327  mofsn2  49335