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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  gencbvex  3509  sscon34b  4256  propeqop  5490  iotanul2  6509  fimacnvinrn2  7067  riota2df  7390  riotaxfrd  7401  fprresex  8306  erinxp  8788  resixp  8930  unxpdomlem3  9217  unfilem1  9264  fsuppunbi  9348  mapfien  9367  marypha1lem  9392  marypha2lem3  9396  suplub  9419  brwdom3  9543  ttrclselem2  9694  r1tr  9747  harcard  9963  acnnum  10035  dfacacn  10124  dfac12lem3  10128  kmlem4  10136  infpss  10198  ackbij1lem12  10212  fin23lem41  10335  fin1a2lem11  10393  fpwwe2lem12  10626  pwfseq  10648  intwun  10719  inttsk  10758  intgru  10798  indval2  12222  xov1plusxeqvd  13524  tpf1o  14538  swrdnznd  14680  pfxccat3  14771  relexpsucnnr  15062  lo1eq  15619  rlimeq  15620  iserex  15708  fsum2dlem  15821  fsumcom2  15825  bcxmas  15889  fprod2dlem  16034  fprodcom2  16038  risefacp1  16082  fallfacp1  16083  rpnnen2lem10  16278  bezoutlem3  16598  eucalgf  16640  prmind2  16742  prmgaplem7  17116  ressabs  17307  mrcuni  17676  mreexmrid  17698  mreexexlem4d  17702  chnso  18679  smndex2dnrinv  18976  dfgrp2  19028  lagsubg  19265  cycsubmcom  19274  gastacl  19378  orbsta2  19383  idrespermg  19480  psgnunilem4  19566  sylow2alem1  19686  efgrelexlemb  19819  unitgrp  20464  unitnegcl  20478  elrhmunit  20592  subrguss  20671  issubdrg  20862  lspsncv0  21249  rspvalint  21348  frlmbas3  21905  psrbagconcl  22056  rhmpsrlem2  22070  psrlidm  22090  psrridm  22091  psrass1  22092  psrcom  22096  mvrcl  22120  mplcoe1  22167  cply1mul  22435  matvscacell  22572  scmatscm  22649  smatvscl  22660  m2detleib  22767  gsummatr01lem3  22793  slesolex  22818  cramerimplem2  22820  ntrdif  23188  clsdif  23189  isclo  23223  neiptoptop  23267  resttopon  23297  cmpfi  23544  conncompconn  23568  2ndcctbss  23591  dis2ndc  23596  dislly  23633  lfinun  23661  dissnref  23664  qtopid  23841  qtopcmplem  23843  trfil1  24022  tgpmulg  24229  utoptop  24370  ucnima  24416  setsmstopn  24614  metustfbas  24693  cfilucfil  24695  tngtopn  24786  bndth  25096  pi1blem  25177  bcth  25467  ovolicc2lem2  25656  ovolicc2  25660  vitalilem1  25746  vitalilem2  25747  vitalilem3  25748  itg2split  25887  ditgsplitlem  25998  limccnp2  26030  dvexp3  26116  radcnv0  26555  abelth2  26581  pilem3  26592  eff1olem  26689  dvloglem  26789  logtayl  26801  asinsinlem  27032  atans2  27072  ppisval2  27245  isppw  27254  chtppilimlem2  27614  chebbnd2  27617  abvcxp  27755  noinfbnd2lem1  27870  legov2  28831  colopp  29026  dfcgra2  29114  prlngsym  29164  usgr1v0e  29642  dfnbgr3  29654  nbusgrf1o0  29685  nb3gr2nb  29700  usgr2pthlem  30078  crctcshwlkn0  30136  wspthnp  30165  2wlkdlem6  30246  elwwlks2ons3im  30269  usgrwwlks2on  30273  umgrwwlks2on  30274  clwwlknclwwlkdifnum  30297  clwwlkf  30364  clwwlknonex2  30426  eupthp1  30533  frgrncvvdeqlem3  30618  ubthlem3  31190  htth  31236  mdslmd4i  32651  mdsymlem3  32723  acunirnmpt  32970  aciunf1lem  32973  aciunf1  32974  suppovss  32992  hashxpe  33118  fsumiunle  33139  xrsmulgzz  33295  gsummpt2co  33334  gsumwrd2dccatlem  33363  cycpmgcl  33439  archiabl  33484  isarchiofld  33485  elrgspnlem4  33531  elrgspnsubrunlem1  33533  fldgensdrg  33601  kerunit  33611  nsgqusf1olem1  33688  nsgqusf1olem3  33690  elrspunidl  33702  dflring3  33753  dflring4  33754  rprmirredb  33788  1arithidom  33793  1arithufdlem4  33803  0ringmon1p  33813  mplvrpmga  33901  mplvrpmmhm  33902  esplyfval3  33928  vieta  33936  lindsun  33981  fedgmul  33987  irngnzply1  34047  lmat22lem  34173  reff  34195  locfinreflem  34196  zarclsiin  34227  pstmfval  34252  rge0scvg  34305  gsumesum  34415  esumrnmpt2  34424  esumfzf  34425  hasheuni  34441  esumcvgsum  34444  esumgect  34446  esum2dlem  34448  esum2d  34449  esumiun  34450  ispisys2  34509  sigapisys  34511  unelldsys  34514  sigapildsys  34518  voliune  34585  oms0  34653  eulerpartlems  34716  eulerpartlemt  34727  actfunsnf1o  34957  actfunsnrndisj  34958  breprexplema  34983  bnj1388  35387  bnj1408  35390  fineqvnttrclse  35503  subfacp1lem3  35640  subfacp1lem5  35642  satffunlem2lem2  35864  elmsta  36006  faclim  36204  fnessref  36834  bj-prmoore  37723  lindsadd  38230  lindsenlbs  38232  poimirlem25  38262  mbfresfi  38283  ftc1anclem6  38315  lkr0f  39836  2polssN  40657  aks4d1p7  42818  primrootspoweq0  42841  aks6d1c4  42859  hashnexinjle  42864  sticksstones1  42881  sticksstones2  42882  sticksstones3  42883  sticksstones10  42890  sticksstones12  42893  aks6d1c6lem3  42907  aks6d1c6isolem1  42909  aks6d1c6isolem2  42910  aks6d1c7  42919  rhmqusspan  42920  grpods  42929  unitscyglem1  42930  unitscyglem2  42931  unitscyglem3  42932  unitscyglem4  42933  unitscyglem5  42934  dford3lem1  43723  dfac21  43763  oninfex2  43942  clsk1indlem3  44739  ntrclsiso  44763  ntrclsk3  44766  ntrclsk13  44767  imo72b2  44868  bcc0  45020  iunincfi  45782  restuni3  45806  suprnmpt  45862  wessf1ornlem  45873  disjf1o  45879  choicefi  45887  mapssbi  45899  unirnmapsn  45900  infnsuprnmpt  45935  fzisoeu  45989  upbdrech  45994  iuneqfzuzlem  46020  supxrleubrnmpt  46090  suprleubrnmpt  46106  infrnmptle  46107  uzub  46115  infxrgelbrnmpt  46138  fprodcn  46286  climsuselem1  46293  climsuse  46294  climeldmeq  46349  climfveq  46353  climfveqf  46364  limsupresico  46384  limsupvaluz  46392  limsupubuz  46397  liminfresico  46455  liminfvalxr  46467  climresdm  46534  xlimresdm  46543  cncfioobdlem  46580  dvbdfbdioo  46614  dvnprodlem2  46631  stoweidlem52  46736  stirlinglem7  46764  stirlinglem10  46767  stirlinglem13  46770  fourierdlem20  46811  fourierdlem25  46816  fourierdlem33  46824  fourierdlem42  46833  fourierdlem57  46847  fourierdlem58  46848  fourierdlem59  46849  fourierdlem65  46855  fourierdlem68  46858  fourierdlem70  46860  fourierdlem71  46861  fourierdlem74  46864  fourierdlem75  46865  fourierdlem80  46870  fourierdlem101  46891  ioorrnopn  46989  ioorrnopnxr  46991  subsaliuncl  47042  sge0rnbnd  47077  sge0lefi  47082  sge0resplit  47090  sge0split  47093  sge0iunmptlemfi  47097  sge0fodjrnlem  47100  sge0iunmpt  47102  sge0isum  47111  sge0xp  47113  sge0seq  47130  sge0reuz  47131  sge0reuzb  47132  ismeannd  47151  psmeasure  47155  meaiuninclem  47164  hoidmv1lelem1  47275  hoidmv1le  47278  hoidmvlelem1  47279  hoidmvle  47284  hoiqssbllem2  47307  opnvonmbllem2  47317  ovolval4lem2  47334  iinhoiicc  47358  vonioo  47366  vonicc  47369  smfaddlem1  47447  smflimlem6  47460  nsssmfmbf  47463  smfresal  47472  smfpimcc  47492  smflimsupmpt  47513  smfliminfmpt  47516  chnerlem1  47568  cfsetsnfsetf  47762  euoreqb  47813  fargshiftfo  48158  paireqne  48227  dfclnbgr3  48558  isuspgrim0lem  48625  isuspgrimlem  48627  usgrgrtrirex  48682  grlimprclnbgrvtx  48731  gpgprismgr4cycllem8  48834  lcoop  49158  lincvalsc0  49168  linc0scn0  49170  snlindsntor  49218  rege1logbrege0  49305  dmrnxp  49582  mofsn2  49590