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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

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 401

This theorem is used by:  gencbvex  3510  sscon34b  4256  propeqop  5489  iotanul2  6509  fimacnvinrn2  7067  riota2df  7392  riotaxfrd  7403  fprresex  8305  erinxp  8787  resixp  8929  unxpdomlem3  9216  unfilem1  9263  fsuppunbi  9347  mapfien  9366  marypha1lem  9391  marypha2lem3  9395  suplub  9418  brwdom3  9542  ttrclselem2  9693  r1tr  9746  harcard  9971  acnnum  10043  dfacacn  10132  dfac12lem3  10136  kmlem4  10144  infpss  10206  ackbij1lem12  10220  fin23lem41  10342  fin1a2lem11  10400  fpwwe2lem12  10633  pwfseq  10655  intwun  10726  inttsk  10765  intgru  10805  indval2  12229  xov1plusxeqvd  13531  tpf1o  14545  swrdnznd  14687  pfxccat3  14778  relexpsucnnr  15069  lo1eq  15626  rlimeq  15627  iserex  15715  fsum2dlem  15828  fsumcom2  15832  bcxmas  15896  fprod2dlem  16041  fprodcom2  16045  risefacp1  16089  fallfacp1  16090  rpnnen2lem10  16285  bezoutlem3  16605  eucalgf  16647  prmind2  16749  prmgaplem7  17123  ressabs  17314  mrcuni  17683  mreexmrid  17705  mreexexlem4d  17709  chnso  18686  smndex2dnrinv  18983  dfgrp2  19035  lagsubg  19272  cycsubmcom  19281  gastacl  19385  orbsta2  19390  idrespermg  19487  psgnunilem4  19573  sylow2alem1  19693  efgrelexlemb  19826  unitgrp  20472  unitnegcl  20486  elrhmunit  20618  subrguss  20697  issubdrg  20894  lspsncv0  21281  rspvalint  21380  frlmbas3  21937  psrbagconcl  22088  rhmpsrlem2  22102  psrlidm  22122  psrridm  22123  psrass1  22124  psrcom  22128  mvrcl  22152  mplcoe1  22199  cply1mul  22467  matvscacell  22604  scmatscm  22681  smatvscl  22692  m2detleib  22799  gsummatr01lem3  22825  slesolex  22850  cramerimplem2  22852  ntrdif  23220  clsdif  23221  isclo  23255  neiptoptop  23299  resttopon  23329  cmpfi  23576  conncompconn  23600  2ndcctbss  23623  dis2ndc  23628  dislly  23665  lfinun  23693  dissnref  23696  qtopid  23873  qtopcmplem  23875  trfil1  24054  tgpmulg  24261  utoptop  24402  ucnima  24448  setsmstopn  24646  metustfbas  24725  cfilucfil  24727  tngtopn  24818  bndth  25128  pi1blem  25209  bcth  25499  ovolicc2lem2  25688  ovolicc2  25692  vitalilem1  25778  vitalilem2  25779  vitalilem3  25780  itg2split  25919  ditgsplitlem  26030  limccnp2  26062  dvexp3  26148  radcnv0  26590  abelth2  26616  pilem3  26627  eff1olem  26724  dvloglem  26824  logtayl  26836  asinsinlem  27067  atans2  27107  ppisval2  27280  isppw  27289  chtppilimlem2  27649  chebbnd2  27652  abvcxp  27790  noinfbnd2lem1  27905  legov2  28866  colopp  29062  dfcgra2  29152  prlngsym  29202  usgr1v0e  29687  dfnbgr3  29699  nbusgrf1o0  29730  nb3gr2nb  29745  usgr2pthlem  30123  crctcshwlkn0  30181  wspthnp  30210  2wlkdlem6  30291  elwwlks2ons3im  30314  usgrwwlks2on  30318  umgrwwlks2on  30319  clwwlknclwwlkdifnum  30342  clwwlkf  30409  clwwlknonex2  30471  eupthp1  30578  frgrncvvdeqlem3  30663  ubthlem3  31235  htth  31281  mdslmd4i  32696  mdsymlem3  32768  acunirnmpt  33015  aciunf1lem  33018  aciunf1  33019  suppovss  33037  hashxpe  33163  fsumiunle  33184  xrsmulgzz  33338  gsummpt2co  33377  gsumwrd2dccatlem  33406  cycpmgcl  33482  archiabl  33527  isarchiofld  33528  elrgspnlem4  33574  elrgspnsubrunlem1  33576  fldgensdrg  33644  kerunit  33654  nsgqusf1olem1  33731  nsgqusf1olem3  33733  elrspunidl  33745  dflring3  33796  dflring4  33797  rprmirredb  33831  1arithidom  33836  1arithufdlem4  33846  0ringmon1p  33856  mplvrpmga  33944  mplvrpmmhm  33945  esplyfval3  33971  vieta  33979  lindsun  34024  fedgmul  34030  irngnzply1  34090  lmat22lem  34216  reff  34238  locfinreflem  34239  zarclsiin  34270  pstmfval  34295  rge0scvg  34348  gsumesum  34458  esumrnmpt2  34467  esumfzf  34468  hasheuni  34484  esumcvgsum  34487  esumgect  34489  esum2dlem  34491  esum2d  34492  esumiun  34493  ispisys2  34552  sigapisys  34554  unelldsys  34557  sigapildsys  34561  voliune  34628  oms0  34696  eulerpartlems  34759  eulerpartlemt  34770  actfunsnf1o  35000  actfunsnrndisj  35001  breprexplema  35026  bnj1388  35430  bnj1408  35433  fineqvnttrclse  35545  subfacp1lem3  35682  subfacp1lem5  35684  satffunlem2lem2  35906  elmsta  36048  faclim  36246  fnessref  36896  bj-prmoore  37785  lindsadd  38292  lindsenlbs  38294  poimirlem25  38324  mbfresfi  38345  ftc1anclem6  38377  lkr0f  39896  2polssN  40717  aks4d1p7  42878  primrootspoweq0  42901  aks6d1c4  42919  hashnexinjle  42924  sticksstones1  42941  sticksstones2  42942  sticksstones3  42943  sticksstones10  42950  sticksstones12  42953  aks6d1c6lem3  42967  aks6d1c6isolem1  42969  aks6d1c6isolem2  42970  aks6d1c7  42979  rhmqusspan  42980  grpods  42989  unitscyglem1  42990  unitscyglem2  42991  unitscyglem3  42992  unitscyglem4  42993  unitscyglem5  42994  dford3lem1  43781  dfac21  43821  oninfex2  44000  clsk1indlem3  44797  ntrclsiso  44821  ntrclsk3  44824  ntrclsk13  44825  imo72b2  44926  bcc0  45078  iunincfi  45840  restuni3  45864  suprnmpt  45920  wessf1ornlem  45931  disjf1o  45937  choicefi  45945  mapssbi  45957  unirnmapsn  45958  infnsuprnmpt  45993  fzisoeu  46047  upbdrech  46052  iuneqfzuzlem  46078  supxrleubrnmpt  46148  suprleubrnmpt  46164  infrnmptle  46165  uzub  46173  infxrgelbrnmpt  46196  fprodcn  46344  climsuselem1  46351  climsuse  46352  climeldmeq  46407  climfveq  46411  climfveqf  46422  limsupresico  46442  limsupvaluz  46450  limsupubuz  46455  liminfresico  46513  liminfvalxr  46525  climresdm  46592  xlimresdm  46601  cncfioobdlem  46638  dvbdfbdioo  46672  dvnprodlem2  46689  stoweidlem52  46794  stirlinglem7  46822  stirlinglem10  46825  stirlinglem13  46828  fourierdlem20  46869  fourierdlem25  46874  fourierdlem33  46882  fourierdlem42  46891  fourierdlem57  46905  fourierdlem58  46906  fourierdlem59  46907  fourierdlem65  46913  fourierdlem68  46916  fourierdlem70  46918  fourierdlem71  46919  fourierdlem74  46922  fourierdlem75  46923  fourierdlem80  46928  fourierdlem101  46949  ioorrnopn  47047  ioorrnopnxr  47049  subsaliuncl  47100  sge0rnbnd  47135  sge0lefi  47140  sge0resplit  47148  sge0split  47151  sge0iunmptlemfi  47155  sge0fodjrnlem  47158  sge0iunmpt  47160  sge0isum  47169  sge0xp  47171  sge0seq  47188  sge0reuz  47189  sge0reuzb  47190  ismeannd  47209  psmeasure  47213  meaiuninclem  47222  hoidmv1lelem1  47333  hoidmv1le  47336  hoidmvlelem1  47337  hoidmvle  47342  hoiqssbllem2  47365  opnvonmbllem2  47375  ovolval4lem2  47392  iinhoiicc  47416  vonioo  47424  vonicc  47427  smfaddlem1  47505  smflimlem6  47518  nsssmfmbf  47521  smfresal  47530  smfpimcc  47550  smflimsupmpt  47571  smfliminfmpt  47574  chnerlem1  47626  cfsetsnfsetf  47823  euoreqb  47874  fargshiftfo  48219  paireqne  48288  dfclnbgr3  48619  isuspgrim0lem  48686  isuspgrimlem  48688  usgrgrtrirex  48743  grlimprclnbgrvtx  48792  gpgprismgr4cycllem8  48895  lcoop  49219  lincvalsc0  49229  linc0scn0  49231  snlindsntor  49279  rege1logbrege0  49366  dmrnxp  49643  mofsn2  49651