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  3506  sscon34b  4249  propeqop  5476  elrelb  5771  iotanul2  6500  fimacnvinrn2  7060  riota2df  7388  riotaxfrd  7399  fprresex  8306  erinxp  8790  resixp  8939  unxpdomlem3  9227  unfilem1  9275  fsuppunbi  9359  mapfien  9378  marypha1lem  9403  marypha2lem3  9407  suplub  9430  brwdom3  9554  ttrclselem2  9705  r1tr  9758  harcard  10031  acnnum  10103  dfacacn  10192  dfac12lem3  10196  kmlem4  10204  infpss  10266  ackbij1lem12  10280  fin23lem41  10402  fin1a2lem11  10460  fpwwe2lem12  10699  pwfseq  10721  intwun  10792  inttsk  10831  intgru  10871  indval2  12295  xov1plusxeqvd  13599  tpf1o  14614  swrdnznd  14758  pfxccat3  14851  relexpsucnnr  15146  lo1eq  15703  rlimeq  15704  iserex  15792  fsum2dlem  15904  fsumcom2  15908  bcxmas  15972  fprod2dlem  16115  fprodcom2  16119  risefacp1  16163  fallfacp1  16164  rpnnen2lem10  16359  bezoutlem3  16679  eucalgf  16721  prmind2  16823  prmgaplem7  17197  ressabs  17388  mrcuni  17757  mreexmrid  17779  mreexexlem4d  17783  chnso  18760  smndex2dnrinv  19076  dfgrp2  19135  lagsubg  19372  cycsubmcom  19381  gastacl  19485  orbsta2  19490  idrespermg  19587  psgnunilem4  19673  sylow2alem1  19793  efgrelexlemb  19926  unitgrp  20575  unitnegcl  20589  elrhmunit  20722  subrguss  20801  issubdrg  20999  lspsncv0  21386  rspvalint  21485  frlmbas3  22044  lindsenlbs  22119  psrbagconcl  22197  rhmpsrlem2  22211  psrlidm  22231  psrridm  22232  psrass1  22233  psrcom  22237  mvrcl  22261  mplcoe1  22308  cply1mul  22576  matvscacell  22713  scmatscm  22790  smatvscl  22801  m2detleib  22908  gsummatr01lem3  22934  slesolex  22962  cramerimplem2  22964  ntrdif  23332  clsdif  23333  isclo  23367  neiptoptop  23411  resttopon  23441  cmpfi  23688  conncompconn  23712  2ndcctbss  23736  dis2ndc  23741  dislly  23778  lfinun  23806  dissnref  23809  qtopid  23986  qtopcmplem  23988  trfil1  24167  tgpmulg  24374  utoptop  24515  ucnima  24561  setsmstopn  24759  metustfbas  24838  cfilucfil  24840  tngtopn  24931  bndth  25241  pi1blem  25322  bcth  25612  ovolicc2lem2  25801  ovolicc2  25805  vitalilem1  25891  vitalilem2  25892  vitalilem3  25893  itg2split  26032  ditgsplitlem  26142  limccnp2  26174  dvexp3  26260  radcnv0  26707  abelth2  26733  pilem3  26744  eff1olem  26840  dvloglem  26940  logtayl  26952  asinsinlem  27183  atans2  27223  ppisval2  27396  isppw  27405  chtppilimlem2  27765  chebbnd2  27768  abvcxp  27906  noinfbnd2lem1  28021  legov2  28983  colopp  29181  dfcgra2  29272  cgraer  29311  cgrabasimass  29312  angmgmlem  29329  prlngsym  29353  usgr1v0e  29841  dfnbgr3  29853  nbusgrf1o0  29884  nb3gr2nb  29899  usgr2pthlem  30283  crctcshwlkn0  30344  wspthnp  30373  2wlkdlem6  30454  elwwlks2ons3im  30477  usgrwwlks2on  30481  umgrwwlks2on  30482  clwwlknclwwlkdifnum  30505  clwwlkf  30572  clwwlknonex2  30634  eupthp1  30751  frgrncvvdeqlem3  30836  ubthlem3  31408  htth  31454  mdslmd4i  32869  mdsymlem3  32941  acunirnmpt  33187  aciunf1lem  33190  aciunf1  33191  suppovss  33208  hashxpe  33333  fsumiunle  33354  xrsmulgzz  33504  gsummpt2co  33543  gsumwrd2dccatlem  33572  cycpmgcl  33648  archiabl  33693  isarchiofld  33694  elrgspnlem4  33740  elrgspnsubrunlem1  33742  fldgensdrg  33810  kerunit  33820  nsgqusf1olem1  33898  nsgqusf1olem3  33900  elrspunidl  33912  dflring3  33963  dflring4  33964  rprmirredb  33998  1arithidom  34003  1arithufdlem4  34013  0ringmon1p  34023  selvply1rhmlem2  34087  mplvrpmmhm  34112  esplyfval3  34138  vieta  34146  lindsun  34191  fedgmul  34197  irngnzply1  34257  lmat22lem  34383  reff  34405  locfinreflem  34406  zarclsiin  34437  pstmfval  34462  rge0scvg  34515  gsumesum  34625  esumrnmpt2  34634  esumfzf  34635  hasheuni  34651  esumcvgsum  34654  esumgect  34656  esum2dlem  34658  esum2d  34659  esumiun  34660  ispisys2  34720  sigapisys  34722  unelldsys  34725  sigapildsys  34729  voliune  34796  oms0  34864  eulerpartlems  34927  eulerpartlemt  34938  actfunsnf1o  35168  actfunsnrndisj  35169  breprexplema  35194  bnj1388  35598  bnj1408  35601  fineqvnttrclse  35717  subfacp1lem3  35868  subfacp1lem5  35870  satffunlem2lem2  36092  elmsta  36234  faclim  36432  fnessref  37067  bj-prmoore  37956  lindsadd  38456  poimirlem25  38483  mbfresfi  38504  ftc1anclem6  38536  lkr0f  40071  2polssN  40892  aks4d1p7  43053  primrootspoweq0  43076  aks6d1c4  43094  hashnexinjle  43099  sticksstones1  43116  sticksstones2  43117  sticksstones3  43118  sticksstones10  43125  sticksstones12  43128  aks6d1c6lem3  43142  aks6d1c6isolem1  43144  aks6d1c6isolem2  43145  aks6d1c7  43154  rhmqusspan  43155  grpods  43164  unitscyglem1  43165  unitscyglem2  43166  unitscyglem3  43167  unitscyglem4  43168  unitscyglem5  43169  dford3lem1  43971  dfac21  44011  oninfex2  44190  clsk1indlem3  44987  ntrclsiso  45011  ntrclsk3  45014  ntrclsk13  45015  imo72b2  45116  bcc0  45268  iunincfi  46030  restuni3  46054  suprnmpt  46110  wessf1ornlem  46121  disjf1o  46127  choicefi  46135  mapssbi  46147  unirnmapsn  46148  infnsuprnmpt  46183  fzisoeu  46237  upbdrech  46242  iuneqfzuzlem  46268  supxrleubrnmpt  46338  suprleubrnmpt  46354  infrnmptle  46355  uzub  46363  infxrgelbrnmpt  46386  fprodcn  46534  climsuselem1  46541  climsuse  46542  climeldmeq  46597  climfveq  46601  climfveqf  46612  limsupresico  46632  limsupvaluz  46640  limsupubuz  46645  liminfresico  46703  liminfvalxr  46715  climresdm  46782  xlimresdm  46791  cncfioobdlem  46828  dvbdfbdioo  46862  dvnprodlem2  46879  stoweidlem52  46984  stirlinglem7  47012  stirlinglem10  47015  stirlinglem13  47018  fourierdlem20  47059  fourierdlem25  47064  fourierdlem33  47072  fourierdlem42  47081  fourierdlem57  47095  fourierdlem58  47096  fourierdlem59  47097  fourierdlem65  47103  fourierdlem68  47106  fourierdlem70  47108  fourierdlem71  47109  fourierdlem74  47112  fourierdlem75  47113  fourierdlem80  47118  fourierdlem101  47139  ioorrnopn  47237  ioorrnopnxr  47239  subsaliuncl  47290  sge0rnbnd  47325  sge0lefi  47330  sge0resplit  47338  sge0split  47341  sge0iunmptlemfi  47345  sge0fodjrnlem  47348  sge0iunmpt  47350  sge0isum  47359  sge0xp  47361  sge0seq  47378  sge0reuz  47379  sge0reuzb  47380  ismeannd  47399  psmeasure  47403  meaiuninclem  47412  hoidmv1lelem1  47523  hoidmv1le  47526  hoidmvlelem1  47527  hoidmvle  47532  hoiqssbllem2  47555  opnvonmbllem2  47565  ovolval4lem2  47582  iinhoiicc  47606  vonioo  47614  vonicc  47617  smfaddlem1  47695  smflimlem6  47708  nsssmfmbf  47711  smfresal  47720  smfpimcc  47740  smflimsupmpt  47761  smfliminfmpt  47764  chnerlem1  47814  sqrtnzqaa  47836  cfsetsnfsetf  48050  euoreqb  48101  fargshiftfo  48446  paireqne  48515  dfclnbgr3  48846  isuspgrim0lem  48913  isuspgrimlem  48915  usgrgrtrirex  48970  grlimprclnbgrvtx  49019  gpgprismgr4cycllem8  49122  lcoop  49445  lincvalsc0  49455  linc0scn0  49457  snlindsntor  49505  rege1logbrege0  49592  dmrnxp  49869  mofsn2  49877