Theorem bilani 505

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 217	. 2 ⊢ (𝜑 → 𝜓)
3	2	adantl 482	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  gencbvex  3490  sscon34b  4239  propeqop  5455  iotanul2  6465  fimacnvinrn2  7020  riota2df  7343  riotaxfrd  7354  fprresex  8257  erinxp  8735  resixp  8878  unxpdomlem3  9165  unfilem1  9212  fsuppunbi  9299  mapfien  9318  marypha1lem  9343  marypha2lem3  9347  suplub  9370  brwdom3  9494  ttrclselem2  9645  r1tr  9698  harcard  9900  acnnum  9972  dfacacn  10062  dfac12lem3  10066  kmlem4  10074  infpss  10136  ackbij1lem12  10150  fin23lem41  10272  fin1a2lem11  10330  fpwwe2lem12  10563  pwfseq  10585  intwun  10656  inttsk  10695  intgru  10735  indval2  12162  xov1plusxeqvd  13449  tpf1o  14461  swrdnznd  14603  pfxccat3  14694  relexpsucnnr  14985  lo1eq  15528  rlimeq  15529  iserex  15617  fsum2dlem  15730  fsumcom2  15734  bcxmas  15798  fprod2dlem  15943  fprodcom2  15947  risefacp1  15992  fallfacp1  15993  rpnnen2lem10  16188  bezoutlem3  16508  eucalgf  16550  prmind2  16652  prmgaplem7  17026  ressabs  17216  mrcuni  17585  mreexmrid  17607  mreexexlem4d  17611  chnso  18588  smndex2dnrinv  18884  dfgrp2  18936  lagsubg  19168  cycsubmcom  19177  gastacl  19282  orbsta2  19287  idrespermg  19384  psgnunilem4  19470  sylow2alem1  19590  efgrelexlemb  19723  unitgrp  20361  unitnegcl  20375  elrhmunit  20489  subrguss  20566  issubdrg  20759  lspsncv0  21146  frlmbas3  21758  psrbagconcl  21909  rhmpsrlem2  21923  psrlidm  21943  psrridm  21944  psrass1  21945  psrcom  21949  mvrcl  21973  mplcoe1  22020  cply1mul  22289  matvscacell  22426  scmatscm  22503  smatvscl  22514  m2detleib  22621  gsummatr01lem3  22647  slesolex  22672  cramerimplem2  22674  ntrdif  23042  clsdif  23043  isclo  23077  neiptoptop  23121  resttopon  23151  cmpfi  23398  conncompconn  23422  2ndcctbss  23445  dis2ndc  23450  dislly  23487  lfinun  23515  dissnref  23518  qtopid  23695  qtopcmplem  23697  trfil1  23876  tgpmulg  24083  utoptop  24224  ucnima  24270  setsmstopn  24468  metustfbas  24547  cfilucfil  24549  tngtopn  24640  bndth  24950  pi1blem  25031  bcth  25321  ovolicc2lem2  25510  ovolicc2  25514  vitalilem1  25600  vitalilem2  25601  vitalilem3  25602  itg2split  25741  ditgsplitlem  25852  limccnp2  25884  dvexp3  25970  radcnv0  26406  abelth2  26432  pilem3  26443  eff1olem  26537  dvloglem  26637  logtayl  26649  asinsinlem  26880  atans2  26920  ppisval2  27093  isppw  27102  chtppilimlem2  27462  chebbnd2  27465  abvcxp  27603  noinfbnd2lem1  27719  legov2  28679  colopp  28862  dfcgra2  28923  usgr1v0e  29420  dfnbgr3  29432  nbusgrf1o0  29463  nb3gr2nb  29478  usgr2pthlem  29856  crctcshwlkn0  29914  wspthnp  29943  2wlkdlem6  30024  elwwlks2ons3im  30047  usgrwwlks2on  30051  umgrwwlks2on  30052  clwwlknclwwlkdifnum  30075  clwwlkf  30142  clwwlknonex2  30204  eupthp1  30311  frgrncvvdeqlem3  30396  ubthlem3  30968  htth  31014  mdslmd4i  32429  mdsymlem3  32501  acunirnmpt  32758  aciunf1lem  32761  aciunf1  32762  suppovss  32780  hashxpe  32906  fsumiunle  32928  xrsmulgzz  33095  gsummpt2co  33136  gsumwrd2dccatlem  33165  cycpmgcl  33241  archiabl  33286  isarchiofld  33287  elrgspnlem4  33333  elrgspnsubrunlem1  33335  fldgensdrg  33405  kerunit  33415  nsgqusf1olem1  33503  nsgqusf1olem3  33505  elrspunidl  33518  rprmirredb  33622  1arithidom  33627  1arithufdlem4  33637  0ringmon1p  33647  mplvrpmga  33736  mplvrpmmhm  33737  esplyfval3  33763  vieta  33771  lindsun  33816  fedgmul  33822  irngnzply1  33882  lmat22lem  34008  reff  34030  locfinreflem  34031  zarclsiin  34062  pstmfval  34087  rge0scvg  34140  gsumesum  34250  esumrnmpt2  34259  esumfzf  34260  hasheuni  34276  esumcvgsum  34279  esumgect  34281  esum2dlem  34283  esum2d  34284  esumiun  34285  ispisys2  34344  sigapisys  34346  unelldsys  34349  sigapildsys  34353  voliune  34420  oms0  34488  eulerpartlems  34551  eulerpartlemt  34562  actfunsnf1o  34795  actfunsnrndisj  34796  breprexplema  34821  bnj1388  35222  bnj1408  35225  fineqvnttrclse  35315  subfacp1lem3  35411  subfacp1lem5  35413  satffunlem2lem2  35635  elmsta  35777  faclim  35975  fnessref  36586  bj-prmoore  37474  lindsadd  37981  lindsenlbs  37983  poimirlem25  38013  mbfresfi  38034  ftc1anclem6  38066  lkr0f  39587  2polssN  40408  aks4d1p7  42569  primrootspoweq0  42592  aks6d1c4  42610  hashnexinjle  42615  sticksstones1  42632  sticksstones2  42633  sticksstones3  42634  sticksstones10  42641  sticksstones12  42644  aks6d1c6lem3  42658  aks6d1c6isolem1  42660  aks6d1c6isolem2  42661  aks6d1c7  42670  rhmqusspan  42671  grpods  42680  unitscyglem1  42681  unitscyglem2  42682  unitscyglem3  42683  unitscyglem4  42684  unitscyglem5  42685  dford3lem1  43472  dfac21  43512  oninfex2  43691  clsk1indlem3  44488  ntrclsiso  44512  ntrclsk3  44515  ntrclsk13  44516  imo72b2  44617  bcc0  44785  iunincfi  45542  restuni3  45566  suprnmpt  45622  wessf1ornlem  45633  disjf1o  45639  choicefi  45647  mapssbi  45659  unirnmapsn  45660  infnsuprnmpt  45695  fzisoeu  45749  upbdrech  45754  iuneqfzuzlem  45780  supxrleubrnmpt  45850  suprleubrnmpt  45866  infrnmptle  45867  uzub  45875  infxrgelbrnmpt  45898  fprodcn  46046  climsuselem1  46053  climsuse  46054  climeldmeq  46109  climfveq  46113  climfveqf  46124  limsupresico  46144  limsupvaluz  46152  limsupubuz  46157  liminfresico  46215  liminfvalxr  46227  climresdm  46294  xlimresdm  46303  cncfioobdlem  46340  dvbdfbdioo  46374  dvnprodlem2  46391  stoweidlem52  46496  stirlinglem7  46524  stirlinglem10  46527  stirlinglem13  46530  fourierdlem20  46571  fourierdlem25  46576  fourierdlem33  46584  fourierdlem42  46593  fourierdlem57  46607  fourierdlem58  46608  fourierdlem59  46609  fourierdlem65  46615  fourierdlem68  46618  fourierdlem70  46620  fourierdlem71  46621  fourierdlem74  46624  fourierdlem75  46625  fourierdlem80  46630  fourierdlem101  46651  ioorrnopn  46749  ioorrnopnxr  46751  subsaliuncl  46802  sge0rnbnd  46837  sge0lefi  46842  sge0resplit  46850  sge0split  46853  sge0iunmptlemfi  46857  sge0fodjrnlem  46860  sge0iunmpt  46862  sge0isum  46871  sge0xp  46873  sge0seq  46890  sge0reuz  46891  sge0reuzb  46892  ismeannd  46911  psmeasure  46915  meaiuninclem  46924  hoidmv1lelem1  47035  hoidmv1le  47038  hoidmvlelem1  47039  hoidmvle  47044  hoiqssbllem2  47067  opnvonmbllem2  47077  ovolval4lem2  47094  iinhoiicc  47118  vonioo  47126  vonicc  47129  smfaddlem1  47207  smflimlem6  47220  nsssmfmbf  47223  smfresal  47232  smfpimcc  47252  smflimsupmpt  47273  smfliminfmpt  47276  chnerlem1  47328  cfsetsnfsetf  47522  euoreqb  47573  fargshiftfo  47918  paireqne  47987  dfclnbgr3  48318  isuspgrim0lem  48385  isuspgrimlem  48387  usgrgrtrirex  48442  grlimprclnbgrvtx  48491  gpgprismgr4cycllem8  48594  lcoop  48903  lincvalsc0  48913  linc0scn0  48915  snlindsntor  48963  rege1logbrege0  49050  dmrnxp  49328  mofsn2  49336