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  3509  sscon34b  4253  propeqop  5488  iotanul2  6510  fimacnvinrn2  7068  riota2df  7396  riotaxfrd  7407  fprresex  8312  erinxp  8794  resixp  8943  unxpdomlem3  9231  unfilem1  9278  fsuppunbi  9362  mapfien  9381  marypha1lem  9406  marypha2lem3  9410  suplub  9433  brwdom3  9557  ttrclselem2  9708  r1tr  9761  harcard  9986  acnnum  10058  dfacacn  10147  dfac12lem3  10151  kmlem4  10159  infpss  10221  ackbij1lem12  10235  fin23lem41  10357  fin1a2lem11  10415  fpwwe2lem12  10654  pwfseq  10676  intwun  10747  inttsk  10786  intgru  10826  indval2  12250  xov1plusxeqvd  13553  tpf1o  14568  swrdnznd  14712  pfxccat3  14805  relexpsucnnr  15100  lo1eq  15657  rlimeq  15658  iserex  15746  fsum2dlem  15858  fsumcom2  15862  bcxmas  15926  fprod2dlem  16071  fprodcom2  16075  risefacp1  16119  fallfacp1  16120  rpnnen2lem10  16315  bezoutlem3  16635  eucalgf  16677  prmind2  16779  prmgaplem7  17153  ressabs  17344  mrcuni  17713  mreexmrid  17735  mreexexlem4d  17739  chnso  18716  smndex2dnrinv  19031  dfgrp2  19090  lagsubg  19327  cycsubmcom  19336  gastacl  19440  orbsta2  19445  idrespermg  19542  psgnunilem4  19628  sylow2alem1  19748  efgrelexlemb  19881  unitgrp  20528  unitnegcl  20542  elrhmunit  20674  subrguss  20753  issubdrg  20950  lspsncv0  21337  rspvalint  21436  frlmbas3  21993  lindsenlbs  22068  psrbagconcl  22146  rhmpsrlem2  22160  psrlidm  22180  psrridm  22181  psrass1  22182  psrcom  22186  mvrcl  22210  mplcoe1  22257  cply1mul  22525  matvscacell  22662  scmatscm  22739  smatvscl  22750  m2detleib  22857  gsummatr01lem3  22883  slesolex  22911  cramerimplem2  22913  ntrdif  23281  clsdif  23282  isclo  23316  neiptoptop  23360  resttopon  23390  cmpfi  23637  conncompconn  23661  2ndcctbss  23685  dis2ndc  23690  dislly  23727  lfinun  23755  dissnref  23758  qtopid  23935  qtopcmplem  23937  trfil1  24116  tgpmulg  24323  utoptop  24464  ucnima  24510  setsmstopn  24708  metustfbas  24787  cfilucfil  24789  tngtopn  24880  bndth  25190  pi1blem  25271  bcth  25561  ovolicc2lem2  25750  ovolicc2  25754  vitalilem1  25840  vitalilem2  25841  vitalilem3  25842  itg2split  25981  ditgsplitlem  26092  limccnp2  26124  dvexp3  26210  radcnv0  26652  abelth2  26678  pilem3  26689  eff1olem  26786  dvloglem  26886  logtayl  26898  asinsinlem  27129  atans2  27169  ppisval2  27342  isppw  27351  chtppilimlem2  27711  chebbnd2  27714  abvcxp  27852  noinfbnd2lem1  27967  legov2  28929  colopp  29127  dfcgra2  29218  cgraer  29257  cgrabasimass  29258  angmgmlem  29275  prlngsym  29299  usgr1v0e  29787  dfnbgr3  29799  nbusgrf1o0  29830  nb3gr2nb  29845  usgr2pthlem  30229  crctcshwlkn0  30290  wspthnp  30319  2wlkdlem6  30400  elwwlks2ons3im  30423  usgrwwlks2on  30427  umgrwwlks2on  30428  clwwlknclwwlkdifnum  30451  clwwlkf  30518  clwwlknonex2  30580  eupthp1  30697  frgrncvvdeqlem3  30782  ubthlem3  31354  htth  31400  mdslmd4i  32815  mdsymlem3  32887  acunirnmpt  33134  aciunf1lem  33137  aciunf1  33138  suppovss  33155  hashxpe  33280  fsumiunle  33301  xrsmulgzz  33451  gsummpt2co  33490  gsumwrd2dccatlem  33519  cycpmgcl  33595  archiabl  33640  isarchiofld  33641  elrgspnlem4  33687  elrgspnsubrunlem1  33689  fldgensdrg  33757  kerunit  33767  nsgqusf1olem1  33844  nsgqusf1olem3  33846  elrspunidl  33858  dflring3  33909  dflring4  33910  rprmirredb  33944  1arithidom  33949  1arithufdlem4  33959  0ringmon1p  33969  selvply1rhmlem2  34033  mplvrpmmhm  34058  esplyfval3  34084  vieta  34092  lindsun  34137  fedgmul  34143  irngnzply1  34203  lmat22lem  34329  reff  34351  locfinreflem  34352  zarclsiin  34383  pstmfval  34408  rge0scvg  34461  gsumesum  34571  esumrnmpt2  34580  esumfzf  34581  hasheuni  34597  esumcvgsum  34600  esumgect  34602  esum2dlem  34604  esum2d  34605  esumiun  34606  ispisys2  34666  sigapisys  34668  unelldsys  34671  sigapildsys  34675  voliune  34742  oms0  34810  eulerpartlems  34873  eulerpartlemt  34884  actfunsnf1o  35114  actfunsnrndisj  35115  breprexplema  35140  bnj1388  35544  bnj1408  35547  fineqvnttrclse  35652  subfacp1lem3  35763  subfacp1lem5  35765  satffunlem2lem2  35987  elmsta  36129  faclim  36327  fnessref  36978  bj-prmoore  37867  lindsadd  38369  poimirlem25  38396  mbfresfi  38417  ftc1anclem6  38449  lkr0f  39969  2polssN  40790  aks4d1p7  42951  primrootspoweq0  42974  aks6d1c4  42992  hashnexinjle  42997  sticksstones1  43014  sticksstones2  43015  sticksstones3  43016  sticksstones10  43023  sticksstones12  43026  aks6d1c6lem3  43040  aks6d1c6isolem1  43042  aks6d1c6isolem2  43043  aks6d1c7  43052  rhmqusspan  43053  grpods  43062  unitscyglem1  43063  unitscyglem2  43064  unitscyglem3  43065  unitscyglem4  43066  unitscyglem5  43067  dford3lem1  43869  dfac21  43909  oninfex2  44088  clsk1indlem3  44885  ntrclsiso  44909  ntrclsk3  44912  ntrclsk13  44913  imo72b2  45014  bcc0  45166  iunincfi  45928  restuni3  45952  suprnmpt  46008  wessf1ornlem  46019  disjf1o  46025  choicefi  46033  mapssbi  46045  unirnmapsn  46046  infnsuprnmpt  46081  fzisoeu  46135  upbdrech  46140  iuneqfzuzlem  46166  supxrleubrnmpt  46236  suprleubrnmpt  46252  infrnmptle  46253  uzub  46261  infxrgelbrnmpt  46284  fprodcn  46432  climsuselem1  46439  climsuse  46440  climeldmeq  46495  climfveq  46499  climfveqf  46510  limsupresico  46530  limsupvaluz  46538  limsupubuz  46543  liminfresico  46601  liminfvalxr  46613  climresdm  46680  xlimresdm  46689  cncfioobdlem  46726  dvbdfbdioo  46760  dvnprodlem2  46777  stoweidlem52  46882  stirlinglem7  46910  stirlinglem10  46913  stirlinglem13  46916  fourierdlem20  46957  fourierdlem25  46962  fourierdlem33  46970  fourierdlem42  46979  fourierdlem57  46993  fourierdlem58  46994  fourierdlem59  46995  fourierdlem65  47001  fourierdlem68  47004  fourierdlem70  47006  fourierdlem71  47007  fourierdlem74  47010  fourierdlem75  47011  fourierdlem80  47016  fourierdlem101  47037  ioorrnopn  47135  ioorrnopnxr  47137  subsaliuncl  47188  sge0rnbnd  47223  sge0lefi  47228  sge0resplit  47236  sge0split  47239  sge0iunmptlemfi  47243  sge0fodjrnlem  47246  sge0iunmpt  47248  sge0isum  47257  sge0xp  47259  sge0seq  47276  sge0reuz  47277  sge0reuzb  47278  ismeannd  47297  psmeasure  47301  meaiuninclem  47310  hoidmv1lelem1  47421  hoidmv1le  47424  hoidmvlelem1  47425  hoidmvle  47430  hoiqssbllem2  47453  opnvonmbllem2  47463  ovolval4lem2  47480  iinhoiicc  47504  vonioo  47512  vonicc  47515  smfaddlem1  47593  smflimlem6  47606  nsssmfmbf  47609  smfresal  47618  smfpimcc  47638  smflimsupmpt  47659  smfliminfmpt  47662  chnerlem1  47712  sqrtnzqaa  47734  cfsetsnfsetf  47948  euoreqb  47999  fargshiftfo  48344  paireqne  48413  dfclnbgr3  48744  isuspgrim0lem  48811  isuspgrimlem  48813  usgrgrtrirex  48868  grlimprclnbgrvtx  48917  gpgprismgr4cycllem8  49020  lcoop  49343  lincvalsc0  49353  linc0scn0  49355  snlindsntor  49403  rege1logbrege0  49490  dmrnxp  49767  mofsn2  49775