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  5478  elrelb  5774  iotanul2  6511  fimacnvinrn2  7072  riota2df  7400  riotaxfrd  7411  fprresex  8329  erinxp  8813  resixp  8962  unxpdomlem3  9250  unfilem1  9298  fsuppunbi  9382  mapfien  9401  marypha1lem  9426  marypha2lem3  9430  suplub  9453  brwdom3  9577  ttrclselem2  9728  r1tr  9784  harcard  10060  acnnum  10132  dfacacn  10221  dfac12lem3  10225  kmlem4  10233  infpss  10295  ackbij1lem12  10309  fin23lem41  10431  fin1a2lem11  10489  fpwwe2lem12  10728  pwfseq  10750  intwun  10821  inttsk  10860  intgru  10900  indval2  12326  xov1plusxeqvd  13630  tpf1o  14647  swrdnznd  14791  pfxccat3  14884  relexpsucnnr  15179  lo1eq  15736  rlimeq  15737  iserex  15825  fsum2dlem  15937  fsumcom2  15941  bcxmas  16005  fprod2dlem  16148  fprodcom2  16152  risefacp1  16196  fallfacp1  16197  rpnnen2lem10  16392  bezoutlem3  16715  eucalgf  16759  prmind2  16861  prmgaplem7  17236  ressabs  17427  mrcuni  17796  mreexmrid  17818  mreexexlem4d  17822  chnso  18799  smndex2dnrinv  19115  dfgrp2  19174  lagsubg  19411  cycsubmcom  19420  gastacl  19524  orbsta2  19529  idrespermg  19626  psgnunilem4  19712  sylow2alem1  19832  efgrelexlemb  19965  unitgrp  20614  unitnegcl  20628  elrhmunit  20761  subrguss  20840  issubdrg  21038  lspsncv0  21425  rspvalint  21524  frlmbas3  22083  lindsenlbs  22158  psrbagconcl  22236  rhmpsrlem2  22250  psrlidm  22270  psrridm  22271  psrass1  22272  psrcom  22276  mvrcl  22300  mplcoe1  22347  cply1mul  22615  matvscacell  22752  scmatscm  22829  smatvscl  22840  m2detleib  22947  gsummatr01lem3  22973  slesolex  23001  cramerimplem2  23003  ntrdif  23371  clsdif  23372  isclo  23406  neiptoptop  23450  resttopon  23480  cmpfi  23727  conncompconn  23751  2ndcctbss  23775  dis2ndc  23780  dislly  23817  lfinun  23845  dissnref  23848  qtopid  24025  qtopcmplem  24027  trfil1  24206  tgpmulg  24413  utoptop  24554  ucnima  24600  setsmstopn  24798  metustfbas  24877  cfilucfil  24879  tngtopn  24970  bndth  25280  pi1blem  25361  bcth  25651  ovolicc2lem2  25840  ovolicc2  25844  vitalilem1  25930  vitalilem2  25931  vitalilem3  25932  itg2split  26071  ditgsplitlem  26181  limccnp2  26213  dvexp3  26299  radcnv0  26744  abelth2  26770  pilem3  26781  eff1olem  26877  dvloglem  26977  logtayl  26989  asinsinlem  27220  atans2  27260  ppisval2  27433  isppw  27442  chtppilimlem2  27802  chebbnd2  27805  abvcxp  27943  noinfbnd2lem1  28088  legov2  29050  colopp  29248  dfcgra2  29339  cgraer  29378  cgrabasimass  29379  angmgmlem  29396  prlngsym  29420  usgr1v0e  29908  dfnbgr3  29920  nbusgrf1o0  29951  nb3gr2nb  29966  usgr2pthlem  30350  crctcshwlkn0  30411  wspthnp  30440  2wlkdlem6  30521  elwwlks2ons3im  30544  usgrwwlks2on  30548  umgrwwlks2on  30549  clwwlknclwwlkdifnum  30572  clwwlkf  30639  clwwlknonex2  30701  eupthp1  30818  frgrncvvdeqlem3  30903  ubthlem3  31475  htth  31521  mdslmd4i  32936  mdsymlem3  33008  acunirnmpt  33296  aciunf1lem  33299  aciunf1  33300  suppovss  33317  hashxpe  33442  fsumiunle  33463  xrsmulgzz  33613  gsummpt2co  33652  gsumwrd2dccatlem  33681  cycpmgcl  33757  archiabl  33802  isarchiofld  33803  elrgspnlem4  33849  elrgspnsubrunlem1  33851  fldgensdrg  33919  kerunit  33929  nsgqusf1olem1  34007  nsgqusf1olem3  34009  elrspunidl  34021  dflring3  34072  dflring4  34073  rprmirredb  34107  1arithidom  34112  1arithufdlem4  34122  0ringmon1p  34132  selvply1rhmlem2  34196  mplvrpmmhm  34221  esplyfval3  34247  vieta  34255  lindsun  34300  fedgmul  34306  irngnzply1  34366  lmat22lem  34492  reff  34514  locfinreflem  34515  zarclsiin  34546  pstmfval  34571  rge0scvg  34624  gsumesum  34734  esumrnmpt2  34743  esumfzf  34744  hasheuni  34760  esumcvgsum  34763  esumgect  34765  esum2dlem  34767  esum2d  34768  esumiun  34769  ispisys2  34829  sigapisys  34831  unelldsys  34834  sigapildsys  34838  voliune  34905  oms0  34972  eulerpartlems  35035  eulerpartlemt  35046  actfunsnf1o  35276  actfunsnrndisj  35277  breprexplema  35302  bnj1388  35706  bnj1408  35709  soinfdom  35761  fineqvnttrclse  35841  j0ltalephlem  35939  subfacp1lem3  36016  subfacp1lem5  36018  satffunlem2lem2  36240  elmsta  36382  faclim  36586  fnessref  37220  bj-prmoore  38111  lindsadd  38612  poimirlem25  38639  mbfresfi  38660  ftc1anclem6  38692  lkr0f  40227  2polssN  41048  aks4d1p7  43209  primrootspoweq0  43232  aks6d1c4  43250  hashnexinjle  43255  sticksstones1  43272  sticksstones2  43273  sticksstones3  43274  sticksstones10  43281  sticksstones12  43284  aks6d1c6lem3  43298  aks6d1c6isolem1  43300  aks6d1c6isolem2  43301  aks6d1c7  43310  rhmqusspan  43311  grpods  43320  unitscyglem1  43321  unitscyglem2  43322  unitscyglem3  43323  unitscyglem4  43324  unitscyglem5  43325  dford3lem1  44109  dfac21  44144  oninfex2  44323  clsk1indlem3  45119  ntrclsiso  45143  ntrclsk3  45146  ntrclsk13  45147  imo72b2  45248  bcc0  45400  iunincfi  46185  restuni3  46209  suprnmpt  46265  wessf1ornlem  46276  disjf1o  46282  choicefi  46290  mapssbi  46302  unirnmapsn  46303  infnsuprnmpt  46338  fzisoeu  46392  upbdrech  46397  iuneqfzuzlem  46422  supxrleubrnmpt  46492  suprleubrnmpt  46508  infrnmptle  46509  uzub  46517  infxrgelbrnmpt  46540  fprodcn  46688  climsuselem1  46695  climsuse  46696  climeldmeq  46751  climfveq  46755  climfveqf  46766  limsupresico  46786  limsupvaluz  46794  limsupubuz  46799  liminfresico  46857  liminfvalxr  46869  climresdm  46936  xlimresdm  46945  cncfioobdlem  46982  dvbdfbdioo  47016  dvnprodlem2  47033  stoweidlem52  47138  stirlinglem7  47166  stirlinglem10  47169  stirlinglem13  47172  fourierdlem20  47213  fourierdlem25  47218  fourierdlem33  47226  fourierdlem42  47235  fourierdlem57  47249  fourierdlem58  47250  fourierdlem59  47251  fourierdlem65  47257  fourierdlem68  47260  fourierdlem70  47262  fourierdlem71  47263  fourierdlem74  47266  fourierdlem75  47267  fourierdlem80  47272  fourierdlem101  47293  ioorrnopn  47391  ioorrnopnxr  47393  subsaliuncl  47444  sge0rnbnd  47479  sge0lefi  47484  sge0resplit  47492  sge0split  47495  sge0iunmptlemfi  47499  sge0fodjrnlem  47502  sge0iunmpt  47504  sge0isum  47513  sge0xp  47515  sge0seq  47532  sge0reuz  47533  sge0reuzb  47534  ismeannd  47553  psmeasure  47557  meaiuninclem  47566  hoidmv1lelem1  47677  hoidmv1le  47680  hoidmvlelem1  47681  hoidmvle  47686  hoiqssbllem2  47709  opnvonmbllem2  47719  ovolval4lem2  47736  iinhoiicc  47760  vonioo  47768  vonicc  47771  smfaddlem1  47849  smflimlem6  47862  nsssmfmbf  47865  smfresal  47874  smfpimcc  47894  smflimsupmpt  47915  smfliminfmpt  47918  chnerlem1  47968  sqrtnzqaa  47990  cfsetsnfsetf  48204  euoreqb  48255  fargshiftfo  48600  paireqne  48669  dfclnbgr3  49000  isuspgrim0lem  49067  isuspgrimlem  49069  usgrgrtrirex  49124  grlimprclnbgrvtx  49173  gpgprismgr4cycllem8  49276  lcoop  49599  lincvalsc0  49609  linc0scn0  49611  snlindsntor  49659  rege1logbrege0  49746  dmrnxp  50023  mofsn2  50031