Theorem anbi1d 643

Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 589	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:  anbi12d  644  anbi1  645  pm5.71  1045  cador  1640  drsb1  2524  eleq1w  2843  eleq1d  2845  clelab  2904  rmoeq1f  3402  rabeq  3426  rabeqbidva  3428  rabeqd  3439  rabeqf  3445  alexeqg  3604  reu2eqd  3693  sbc2or  3747  sbc5ALT  3767  psstr  4034  difin2  4245  r19.28z  4457  dfif6  4484  rabsneq  4599  rexreusng  4636  reurexprg  4661  rabsnifsb  4679  ssunsn2  4782  preq12bg  4807  opeq1  4839  eluni  4869  csbuni  4897  unissb  4900  iuneq12d  4979  disjxun  5100  unopab  5184  mpteq12da  5187  mpteq12f  5189  mpteq12dva  5190  dftr2c  5214  axrep1  5232  axreplem  5233  zfrepclf  5243  axsepgfromrep  5246  axsepg  5249  sepg  5250  zfausclOLD  5252  reusv2lem4  5363  rabxfrd  5379  opthg  5446  otthg  5454  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  opeqsng  5475  euotd  5486  elopabw  5500  pocl  5567  xpeq1  5665  elxpi  5673  vtoclr  5714  opbrop  5750  dmopab2rex  5900  resopab2  6030  rnco  6256  dflim2  6424  dffun2  6553  fun11  6619  feq2  6693  f1eq2  6779  f1eq3  6780  foeq2  6798  brprcneu  6880  brprcneuALT  6881  ssimaexg  6976  dmfco  6986  funcnvmpt  7000  fndmdif  7046  respreima  7070  isoeq5  7333  isoini  7350  isopolem  7357  f1oiso  7363  f1oiso2  7364  riotaeqdv  7382  oprabidw  7455  oprabid  7456  oprabv  7484  mpoeq123  7496  mpoeq123dva  7498  0mpo0  7507  eloprabga  7533  resoprab  7542  resoprab2  7543  elrnmpores  7562  ov  7568  ov3  7587  ov6g  7588  ovg  7589  imaeqexov  7663  mpt3fvd  7692  caoftrn  7738  uniuni  7780  limuni3  7867  elxp4  7938  elxp5  7939  opabex3d  7981  opabex3rd  7982  opabex3  7983  releldmdifi  8061  opiota  8075  eloprabi  8079  mptmpoopabbrd  8099  cnvf1o  8129  frxp  8145  xporderlem  8146  poxp  8147  fnwelem  8150  poxp2  8167  xpord3pred  8176  poseq  8182  soseq  8183  suppimacnv  8199  rexsupp  8207  mpocurryd  8294  smoel2  8379  omeu  8601  oeeui  8619  omabs  8668  omopth  8679  eldifsucnn  8681  qliftel  8829  brecop  8839  eroveu  8841  erov  8843  ecopovtrn  8849  curf  8898  ixpsnf1o  8974  dom2lem  9027  mapsnend  9072  xpsnen  9088  xpassen  9098  pw2f1olem  9108  xpf1o  9166  unxpdom  9258  domunfican  9321  preleqALT  9625  zfinf  9647  cantnfs  9674  brttrcl  9721  ttrclselem2  9734  tcvalg  9744  r0weon  10098  fseqenlem1  10110  acni2  10132  aceq1  10203  aceq0  10204  dfac5lem4  10212  dfac2a  10215  dfac12lem2  10230  cardcf  10336  cfeq0  10341  cfsuc  10342  cff1  10343  cfss  10350  isf32lem5  10442  fin1a2lem6  10490  zfac  10545  brdom7disj  10617  brdom6disj  10618  axrepnd  10686  axunndlem1  10687  axinfnd  10698  axacndlem5  10703  axacnd  10704  zfcndrep  10706  zfcndinf  10710  zfcndac  10711  pwfseqlem4a  10753  pwfseqlem4  10754  gruina  10910  grothomex  10921  ordpipq  11034  elnpi  11080  genpass  11101  ltprord  11122  reclem2pr  11140  reclem3pr  11141  recexpr  11143  addsrmo  11165  mulsrmo  11166  addsrpr  11167  mulsrpr  11168  ltsosr  11186  mulgt0sr  11197  supsr  11204  ltresr  11232  axpre-lttrn  11258  axpre-mulgt0  11260  prime  12787  peano5uzti  12796  rexuz  13032  ltxr  13251  qbtwnre  13336  xmulneg1  13406  supxr2  13451  ixxval  13491  fzval  13648  preduz  13791  nn0opth2  14423  hashbclem  14604  hashf1lem2  14608  eqwrd  14709  pfxeq  14853  wrd2ind  14880  cshwcsh2id  14987  eqwrds3  15123  cleq1lem  15144  rtrclreclem3  15222  rtrclreclem4  15223  relexpindlem  15225  abslt  15491  absle  15492  lenegsq  15497  abs2difabs  15511  ello12  15692  elo12  15703  o1lo1  15713  rlimuni  15726  lo1resb  15740  o1resb  15742  2clim  15748  rlimcn3  15766  climcn2  15769  addcn2  15770  mulcn2  15772  o1of2  15789  sumeq1  15865  fsum2dlem  15945  modfsummod  15970  prodeq1f  16084  prodeq1  16085  fprod2dlem  16156  nndivdvds  16440  divalg2  16584  smupval  16667  gcdval  16675  gcdass  16729  lcmval  16776  lcmass  16798  rpexp  16907  pythagtriplem2  17004  pythagtrip  17021  vdwapun  17161  0ram  17207  ramub1lem2  17214  pwsle  17673  imasleval  17722  ismre  17769  ismri  17814  iscatd2  17864  dfiso2  17956  isssc  18004  funcpropd  18086  fullpropd  18106  fthres2b  18116  fthres2c  18117  setcsect  18273  cat1lem  18280  cat1  18281  prslem  18480  drsdir  18485  posi  18500  tosso  18600  odudlatb  18708  ipoval  18713  ipolt  18718  dirge  18786  mgmidpfod  18866  gsumpropd2lem  18877  mgmhmpropd  18896  issgrpv  18919  issgrpn0  18920  ismhm0  18994  mhmpropd  18996  mndind  19033  mgmnsgrpex  19139  issubg3  19364  isga  19514  symgfixelq  19656  psgnfval  19723  psgnval  19730  dprdw  20235  subgdmdprd  20259  isomnd  20346  isrnghm  20680  issubrg  20832  resrhm2b  20863  rngcsect  20897  rngcinv  20898  ringcsect  20931  ringcinv  20932  drngpropd  21036  orngmul  21131  islmod  21148  lmodlema  21149  lmodprop2d  21208  lsslss  21245  lbspropd  21383  lbsacsbs  21443  isfieldidl2  21550  znleval  21869  islbs4  22147  islinds3  22149  aspval2  22215  psrbag  22234  pf1ind  22682  mdetunilem4  22939  mdetunilem9  22944  istopg  23222  basis2  23278  tg2  23292  iscld  23354  isnei  23430  isneip  23432  neiptoptop  23458  neiptopnei  23459  neitr  23507  restlp  23510  iscn  23562  cnpval  23563  iscnp  23564  regsep  23661  1stcclb  23771  2ndc1stc  23778  2ndcctbss  23783  2ndcdisj  23784  llyi  23802  nllyi  23803  hausmapdom  23828  locfinnei  23851  comppfsc  23860  elkgen  23864  txbas  23895  txcls  23932  txcnpi  23936  ptpjopn  23940  txdis1cn  23963  txtube  23968  txcmplem1  23969  hausdiag  23973  tx1stc  23978  txkgen  23980  xkococn  23988  elqtop  24025  kqreglem1  24069  elmptrab  24155  isfbas  24157  elflim2  24292  elflim  24299  hauspwpwf1  24315  alexsublem  24372  ghmcnp  24443  qustgplem  24449  tsmssubm  24471  elutop  24561  ustuqtop4  24572  isucn  24605  iscfilu  24615  ispsmet  24632  ismet  24651  isxmet  24652  ismet2  24661  imasdsf1olem  24701  blres  24759  elmopn  24770  mopni  24820  neibl  24829  nrmmetd  24902  ngppropd  24965  elcncf  25219  mulc1cncf  25235  elpi1  25375  isclmp  25427  metcld2  25637  pmltpclem1  25778  itg1climres  26044  itg2val  26058  isibl  26095  itgeq1f  26101  itgeq1  26102  cbvitgv  26106  itgresr  26108  iblcn  26128  itgfsum  26156  dvreslem  26238  dvfsumlem2  26356  deg1ldg  26419  vieta1  26644  ulm2  26721  sincosq2sgn  26837  sincosq4sgn  26839  efopn  26995  dvdsflsumcom  27524  fsumvma2  27550  logfac2  27553  dchrptlem1  27600  lgsdchrval  27690  2lgslem1a  27727  pntibndlem3  27928  pntlemi  27940  pntleme  27944  pnt3  27948  ltsval  28013  nolt02o  28061  leltstr  28127  nocvxminlem  28149  madebday  28295  ltslpss  28303  addsprop  28371  mulsproplemcbv  28510  mulsproplem1  28511  mulsprop  28525  abslts  28644  eucliddivs  28771  bdayfinbndlem2  28863  z12sge0  28878  istrkgld  28930  istrkg2ld  28931  istrkg3ld  28932  axtgsegcon  28935  axtg5seg  28936  axtgpasch  28938  axtgupdim2  28942  legov  29057  islnopp  29224  ishpg  29246  iscgra1  29326  dfcgra2  29347  elcgrabasi  29384  dfcgrg2  29417  brprlng  29425  brcgr  29487  brbtwn2  29492  axsegconlem1  29504  axsegcon  29514  axcontlem10  29560  edgssv2  29788  uhgr2edg  29798  isfusgrf1  29910  edgnbusgreu  29957  cplgr3v  30025  vtxdun  30071  upgr2wlk  30256  upgrtrls  30293  upgristrl  30294  upgrf1istrl  30295  dfpth2  30323  2pthnloop  30326  usgr2pth  30359  isclwlke  30373  isclwlkupgr  30374  iswwlksnx  30438  wlknewwlksn  30485  2pthon3v  30541  elwwlks2on  30559  wpthswwlks2on  30562  rusgrnumwwlkl1  30569  rusgrnumwwlkb0  30572  clwwlknp  30637  clwwlkf  30647  erclwwlknsym  30670  erclwwlkntr  30671  clwwlknonwwlknonb  30706  0trl  30722  0spth  30726  0crct  30733  0cycl  30734  isacycgr  30760  upgr4cycl4dv4e  30795  upgriseupth  30817  eupth2lem2  30829  3cyclfrgrrn1  30895  4cycl2vnunb  30900  frgrncvvdeqlem2  30910  frgr2wwlk1  30939  fusgr2wsp2nb  30944  numclwlk1lem1  30979  vciOLD  31172  isvclem  31188  nmoofval  31373  isph  31433  norm3lemt  31763  isch2  31834  cmbr  32195  eigre  32446  eigorth  32449  nmopub  32519  nmfnleub  32536  cvbr  32893  mdbr  32905  dmdbr  32910  chrelat2  32981  mdsymlem2  33015  rexunirn  33139  ifeqeqx  33189  iunrnmptss  33210  fdifsupp  33329  ressupprn  33334  1stpreima  33351  fpwrelmapffslem  33374  archirng  33799  isslmd  33813  slmdlema  33814  urpropd  33841  lindflbs  33984  islbs5  33985  lindfpropd  33987  opprqus0g  34064  idlsrgval  34085  ressply1mon1p  34150  ccfldextdgrr  34354  constrsslem  34423  constrconj  34427  constrlccllem  34435  constrcbvlem  34437  dya2iocuni  34965  omsfval  34976  elcarsg  34987  itgeq12dv  35008  isrrvv  35125  reprinrn  35297  reprdifc  35306  istrkg2d  35345  axtgupdim2ALTV  35347  brafs  35354  bnj956  35457  bnj1146  35471  bnj18eq1  35607  omeueq  35773  axsepg2  35876  axsepg3  35877  axsepg3ALT  35878  axsepg4  35879  axsepg5  35880  zltp1ne  36008  kur14  36099  pconncn  36107  cnpconn  36113  txpconn  36115  cvmscbv  36141  cvmcov  36146  cvmsi  36148  cvmsval  36149  cvmopnlem  36161  cvmlift2lem10  36195  cvmlift3lem2  36203  cvmlift3lem6  36207  cvmlift3lem7  36208  cvmlift3lem9  36210  cvmlift3  36211  satf0op  36260  sat1el2xp  36262  satffunlem  36284  dmopab3rexdif  36288  mclsssvlem  36445  mclsind  36453  rexxfr3dALT  36522  eldm3  36650  opelco3  36663  dfon2lem6  36674  dfon2lem7  36675  dfon2lem8  36676  dfon2  36678  elfuns  36801  lemsuccf  36827  brofs  36894  5segofs  36895  brifs  36932  ifscgr  36933  brcolinear  36948  lineext  36965  brfs  36968  fscgr  36969  linecgr  36970  btwnconn1lem4  36979  btwnconn1lem8  36983  btwnconn1lem11  36986  btwnconn1lem12  36987  segcon2  36994  brsegle  36997  outsideofeq  37019  funray  37029  funline  37031  fvline  37033  linethru  37042  disjeq12dv  37128  prodeq12sdv  37131  itgeq12sdv  37132  cbvitgvw2  37161  cbvitgdavw  37194  cbvitgdavw2  37210  trer  37228  finminlem  37230  ivthALT  37247  filnetlem4  37293  axtco1  37385  axtco1from2  37387  ttcexg  37444  mh-infprim1bi  37458  knoppndvlem21  37522  bj-sepg  37960  bj-elgab  37976  bj-imdirvallem  38238  csboprabg  38390  topdifinffinlem  38407  icoreval  38413  isbasisrelowllem1  38415  isbasisrelowllem2  38416  relowlssretop  38423  pibp19  38474  ptrest  38674  poimirlem1  38676  poimirlem13  38688  poimirlem14  38689  poimirlem22  38697  poimirlem24  38699  poimirlem26  38701  poimirlem27  38702  heicant  38710  mblfinlem3  38714  mblfinlem4  38715  mbfresfi  38721  itg2addnclem3  38728  itg2addnc  38729  itg2gt0cn  38730  areacirclem5  38767  cover2  38786  cover2g  38787  fdc  38816  fdc1  38817  heibor1  38881  bfp  38895  rngosn3  38995  drngoi  39022  isdrngo1  39027  isriscg  39055  isfldidl2  39140  raldmqseu  39434  eldmxrncnvepres  39503  brressn  39600  islshpat  40211  lcvbr  40215  lshpsmreu  40303  ldual1dim  40360  cvrval  40463  cvrnbtwn3  40470  iscvlat2N  40518  ishlat3N  40548  hlrelat5N  40595  3dim0  40651  llnexatN  40715  islpln5  40729  islvol5  40773  pmapjat1  41047  ltrnu  41315  cdleme02N  41416  cdlemg33b  41901  cdlemg33c  41902  dvhb1dimN  42180  dibelval3  42341  dibopelval3  42342  dib1dim  42359  dibglbN  42360  diblsmopel  42365  dicval  42370  dicopelval  42371  dicelval3  42374  dicelval1sta  42381  dihopelvalcpre  42442  dih1dimatlem  42523  dihpN  42530  dihjatcclem4  42615  lpolsetN  42676  mapdpglem3  42869  hdmapglem7a  43121  sticksstones23  43356  exfinfldd  43390  fimgmcyclem  43734  fimgmcyc  43735  fsuppind  43755  fsuppssindlem2  43757  prjspeclsp  43777  mrefg2  43855  mzpclval  43873  eldiophb  43905  eldioph2lem1  43908  eldioph3  43914  lzenom  43918  diophin  43920  eldiophss  43922  diophrex  43923  eq0rabdioph  43924  pellexlem3  43975  elpell1qr  43991  elpell14qr  43993  elpell1234qr  43995  jm2.27  44152  rmydioph  44158  expdiophlem1  44165  expdioph  44167  pw2f1ocnv  44181  hbtlem1  44262  hbtlem7  44264  dgraalem  44284  dgraaub  44287  dflim7  44412  omabs2  44471  tfsconcatfv2  44479  tfsconcat0i  44484  nadd1suc  44531  ifpbi2  44605  inintabd  44717  cnvcnvintabd  44737  cnvintabd  44740  clcnvlem  44760  iunrelexpmin1  44845  uneqsn  45162  k0004lem2  45285  mnuprdlem1  45393  mnuprdlem2  45394  binomcxplemnotnn0  45477  2sbc6g  45536  2sbc5g  45537  iotasbc  45539  dropab1  45566  dropab2  45567  relpeq5  46074  modelaxreplem3  46106  omssaxinf2  46114  brpermmodel  46129  permaxinf2lem  46138  cbvmpo1  46249  r19.28zf  46310  disjinfi  46343  dmrelrnrel  46375  mullimc  46764  mullimcf  46771  limsuppnfd  46848  limsuppnf  46857  limsupre2  46871  limsupre2mpt  46876  limsupre3  46879  limsupre3mpt  46880  limsupre3uzlem  46881  fourierdlem42  47295  fourierdlem48  47300  fourierdlem50  47302  fourierdlem51  47303  fourierdlem54  47306  fourierdlem86  47338  ovnval2  47691  ovnsubaddlem1  47716  hoiqssbl  47771  vonicclem2  47830  f1cof1b  48283  f1ocof1ob2  48288  funressnbrafv2  48450  dfatdmfcoafv2  48460  2ffzoeq  48534  fundcmpsurbijinj  48628  ichreuopeq  48691  prproropf1olem4  48724  prprspr2  48736  prprsprreu  48737  prprreueq  48738  reuopreuprim  48744  nprmmul3  48747  isubgrgrim  49163  grtriprop  49175  isgrtri  49177  opgpgvtx  49289  pgnbgreunbgrlem1  49347  pgnbgreunbgrlem4  49353  grlimedgnedg  49365  rngcsectALTV  49508  rngcinvALTV  49509  ringcsectALTV  49542  ringcinvALTV  49543  lmod1  49740  elbigo2  49800  prelrrx2bd  49962  rrx2vlinest  49989  eloprab1st2nd  50115  i0oii  50170  io1ii  50171  lubeldm2d  50208  glbeldm2d  50209  sectpropdlem  50286  invpropdlem  50288  isopropdlem  50290  uppropd  50433  functhinc  50719  fullthinc  50721