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  1641  drsb1  2525  eleq1w  2844  eleq1d  2846  clelab  2905  rmoeq1f  3403  rabeq  3427  rabeqbidva  3429  rabeqd  3440  rabeqf  3446  alexeqg  3605  reu2eqd  3694  sbc2or  3748  sbc5ALT  3768  rexssOLD  4007  psstr  4056  difin2  4247  r19.28z  4458  dfif6  4485  rabsneq  4603  rexreusng  4640  reurexprg  4665  rabsnifsb  4683  ssunsn2  4788  preq12bg  4813  opeq1  4833  eluni  4870  csbuni  4898  unissb  4901  iuneq12d  4980  disjxun  5101  unopab  5185  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  dftr2c  5215  axrep1  5233  axreplem  5234  zfrepclf  5244  axsepgfromrep  5247  axsepg  5250  sepg  5251  zfausclOLD  5253  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  5749  dmopab2rex  5899  resopab2  6028  rnco  6253  dflim2  6421  dffun2  6548  fun11  6614  feq2  6688  f1eq2  6774  f1eq3  6775  foeq2  6793  brprcneu  6875  brprcneuALT  6876  ssimaexg  6971  dmfco  6981  funcnvmpt  6995  fndmdif  7041  respreima  7065  isoeq5  7329  isoini  7346  isopolem  7353  f1oiso  7359  f1oiso2  7360  riotaeqdv  7378  oprabidw  7451  oprabid  7452  oprabv  7480  mpoeq123  7492  mpoeq123dva  7494  0mpo0  7503  eloprabga  7529  resoprab  7538  resoprab2  7539  elrnmpores  7558  ov  7564  ov3  7583  ov6g  7584  ovg  7585  imaeqexov  7659  mpt3fvd  7688  caoftrn  7734  uniuni  7776  limuni3  7863  elxp4  7934  elxp5  7935  opabex3d  7977  opabex3rd  7978  opabex3  7979  releldmdifi  8056  opiota  8070  eloprabi  8074  mptmpoopabbrd  8094  cnvf1o  8122  frxp  8138  xporderlem  8139  poxp  8140  fnwelem  8143  poxp2  8160  xpord3pred  8169  poseq  8175  soseq  8176  suppimacnv  8191  rexsupp  8199  mpocurryd  8286  smoel2  8371  omeu  8593  oeeui  8611  omabs  8660  omopth  8671  eldifsucnn  8673  qliftel  8821  brecop  8831  eroveu  8833  erov  8835  ecopovtrn  8841  curf  8890  ixpsnf1o  8966  dom2lem  9019  mapsnend  9064  xpsnen  9080  xpassen  9090  pw2f1olem  9100  xpf1o  9158  unxpdom  9250  domunfican  9313  preleqALT  9618  zfinf  9640  cantnfs  9667  brttrcl  9714  ttrclselem2  9727  tcvalg  9737  r0weon  10091  fseqenlem1  10103  acni2  10125  aceq1  10196  aceq0  10197  dfac5lem4  10205  dfac2a  10208  dfac12lem2  10223  cardcf  10329  cfeq0  10334  cfsuc  10335  cff1  10336  cfss  10343  isf32lem5  10435  fin1a2lem6  10483  zfac  10538  brdom7disj  10610  brdom6disj  10611  axrepnd  10679  axunndlem1  10680  axinfnd  10691  axacndlem5  10696  axacnd  10697  zfcndrep  10699  zfcndinf  10703  zfcndac  10704  pwfseqlem4a  10746  pwfseqlem4  10747  gruina  10903  grothomex  10914  ordpipq  11027  elnpi  11073  genpass  11094  ltprord  11115  reclem2pr  11133  reclem3pr  11134  recexpr  11136  addsrmo  11158  mulsrmo  11159  addsrpr  11160  mulsrpr  11161  ltsosr  11179  mulgt0sr  11190  supsr  11197  ltresr  11225  axpre-lttrn  11251  axpre-mulgt0  11253  prime  12780  peano5uzti  12789  rexuz  13025  ltxr  13244  qbtwnre  13329  xmulneg1  13399  supxr2  13444  ixxval  13484  fzval  13641  preduz  13784  nn0opth2  14416  hashbclem  14597  hashf1lem2  14601  eqwrd  14702  pfxeq  14845  wrd2ind  14872  cshwcsh2id  14979  eqwrds3  15114  cleq1lem  15135  rtrclreclem3  15213  rtrclreclem4  15214  relexpindlem  15216  abslt  15482  absle  15483  lenegsq  15488  abs2difabs  15502  ello12  15683  elo12  15694  o1lo1  15704  rlimuni  15717  lo1resb  15731  o1resb  15733  2clim  15739  rlimcn3  15757  climcn2  15760  addcn2  15761  mulcn2  15763  o1of2  15780  sumeq1  15856  fsum2dlem  15936  modfsummod  15961  prodeq1f  16075  prodeq1  16076  fprod2dlem  16147  nndivdvds  16431  divalg2  16575  smupval  16658  gcdval  16666  gcdass  16720  lcmval  16767  lcmass  16789  rpexp  16898  pythagtriplem2  16995  pythagtrip  17012  vdwapun  17152  0ram  17198  ramub1lem2  17205  pwsle  17664  imasleval  17713  ismre  17760  ismri  17805  iscatd2  17855  dfiso2  17947  isssc  17995  funcpropd  18077  fullpropd  18097  fthres2b  18107  fthres2c  18108  setcsect  18264  cat1lem  18271  cat1  18272  prslem  18471  drsdir  18476  posi  18491  tosso  18591  odudlatb  18699  ipoval  18704  ipolt  18709  dirge  18777  mgmidpfod  18857  gsumpropd2lem  18868  mgmhmpropd  18887  issgrpv  18910  issgrpn0  18911  ismhm0  18985  mhmpropd  18987  mndind  19024  mgmnsgrpex  19130  issubg3  19355  isga  19505  symgfixelq  19647  psgnfval  19714  psgnval  19721  dprdw  20226  subgdmdprd  20250  isomnd  20337  isrnghm  20671  issubrg  20823  resrhm2b  20854  rngcsect  20888  rngcinv  20889  ringcsect  20922  ringcinv  20923  drngpropd  21027  orngmul  21122  islmod  21139  lmodlema  21140  lmodprop2d  21199  lsslss  21236  lbspropd  21374  lbsacsbs  21434  isfieldidl2  21541  znleval  21860  islbs4  22138  islinds3  22140  aspval2  22206  psrbag  22225  pf1ind  22673  mdetunilem4  22930  mdetunilem9  22935  istopg  23213  basis2  23269  tg2  23283  iscld  23345  isnei  23421  isneip  23423  neiptoptop  23449  neiptopnei  23450  neitr  23498  restlp  23501  iscn  23553  cnpval  23554  iscnp  23555  regsep  23652  1stcclb  23762  2ndc1stc  23769  2ndcctbss  23774  2ndcdisj  23775  llyi  23793  nllyi  23794  hausmapdom  23819  locfinnei  23842  comppfsc  23851  elkgen  23855  txbas  23886  txcls  23923  txcnpi  23927  ptpjopn  23931  txdis1cn  23954  txtube  23959  txcmplem1  23960  hausdiag  23964  tx1stc  23969  txkgen  23971  xkococn  23979  elqtop  24016  kqreglem1  24060  elmptrab  24146  isfbas  24148  elflim2  24283  elflim  24290  hauspwpwf1  24306  alexsublem  24363  ghmcnp  24434  qustgplem  24440  tsmssubm  24462  elutop  24552  ustuqtop4  24563  isucn  24596  iscfilu  24606  ispsmet  24623  ismet  24642  isxmet  24643  ismet2  24652  imasdsf1olem  24692  blres  24750  elmopn  24761  mopni  24811  neibl  24820  nrmmetd  24893  ngppropd  24956  elcncf  25210  mulc1cncf  25226  elpi1  25366  isclmp  25418  metcld2  25628  pmltpclem1  25769  itg1climres  26035  itg2val  26049  isibl  26086  itgeq1f  26092  itgeq1  26093  cbvitgv  26097  itgresr  26099  iblcn  26119  itgfsum  26147  dvreslem  26229  dvfsumlem2  26347  deg1ldg  26410  vieta1  26635  ulm2  26712  sincosq2sgn  26828  sincosq4sgn  26830  efopn  26986  dvdsflsumcom  27515  fsumvma2  27541  logfac2  27544  dchrptlem1  27591  lgsdchrval  27681  2lgslem1a  27718  pntibndlem3  27919  pntlemi  27931  pntleme  27935  pnt3  27939  ltsval  28004  nolt02o  28052  leltstr  28118  nocvxminlem  28140  madebday  28286  ltslpss  28294  addsprop  28362  mulsproplemcbv  28501  mulsproplem1  28502  mulsprop  28516  abslts  28635  eucliddivs  28762  bdayfinbndlem2  28854  z12sge0  28869  istrkgld  28921  istrkg2ld  28922  istrkg3ld  28923  axtgsegcon  28926  axtg5seg  28927  axtgpasch  28929  axtgupdim2  28933  legov  29048  islnopp  29215  ishpg  29237  iscgra1  29317  dfcgra2  29338  elcgrabasi  29375  dfcgrg2  29408  brprlng  29416  brcgr  29478  brbtwn2  29483  axsegconlem1  29495  axsegcon  29505  axcontlem10  29551  edgssv2  29779  uhgr2edg  29789  isfusgrf1  29901  edgnbusgreu  29948  cplgr3v  30016  vtxdun  30062  upgr2wlk  30247  upgrtrls  30284  upgristrl  30285  upgrf1istrl  30286  dfpth2  30314  2pthnloop  30317  usgr2pth  30350  isclwlke  30364  isclwlkupgr  30365  iswwlksnx  30429  wlknewwlksn  30476  2pthon3v  30532  elwwlks2on  30550  wpthswwlks2on  30553  rusgrnumwwlkl1  30560  rusgrnumwwlkb0  30563  clwwlknp  30628  clwwlkf  30638  erclwwlknsym  30661  erclwwlkntr  30662  clwwlknonwwlknonb  30697  0trl  30713  0spth  30717  0crct  30724  0cycl  30725  isacycgr  30751  upgr4cycl4dv4e  30786  upgriseupth  30808  eupth2lem2  30820  3cyclfrgrrn1  30886  4cycl2vnunb  30891  frgrncvvdeqlem2  30901  frgr2wwlk1  30930  fusgr2wsp2nb  30935  numclwlk1lem1  30970  vciOLD  31163  isvclem  31179  nmoofval  31364  isph  31424  norm3lemt  31754  isch2  31825  cmbr  32186  eigre  32437  eigorth  32440  nmopub  32510  nmfnleub  32527  cvbr  32884  mdbr  32896  dmdbr  32901  chrelat2  32972  mdsymlem2  33006  rexunirn  33088  ifeqeqx  33138  iunrnmptss  33159  fdifsupp  33278  ressupprn  33283  1stpreima  33300  fpwrelmapffslem  33324  archirng  33749  isslmd  33763  slmdlema  33764  urpropd  33791  lindflbs  33934  islbs5  33935  lindfpropd  33937  opprqus0g  34014  idlsrgval  34035  ressply1mon1p  34100  ccfldextdgrr  34304  constrsslem  34373  constrconj  34377  constrlccllem  34385  constrcbvlem  34387  dya2iocuni  34915  omsfval  34926  elcarsg  34937  itgeq12dv  34958  isrrvv  35075  reprinrn  35247  reprdifc  35256  istrkg2d  35295  axtgupdim2ALTV  35297  brafs  35304  bnj956  35407  bnj1146  35421  bnj18eq1  35557  axsepg2  35808  axsepg3  35809  axsepg3ALT  35810  axsepg4  35811  axsepg5  35812  zltp1ne  35900  kur14  35981  pconncn  35989  cnpconn  35995  txpconn  35997  cvmscbv  36023  cvmcov  36028  cvmsi  36030  cvmsval  36031  cvmopnlem  36043  cvmlift2lem10  36077  cvmlift3lem2  36085  cvmlift3lem6  36089  cvmlift3lem7  36090  cvmlift3lem9  36092  cvmlift3  36093  satf0op  36142  sat1el2xp  36144  satffunlem  36166  dmopab3rexdif  36170  mclsssvlem  36327  mclsind  36335  rexxfr3dALT  36404  eldm3  36526  opelco3  36539  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  dfon2  36554  elfuns  36677  lemsuccf  36703  brofs  36770  5segofs  36771  brifs  36808  ifscgr  36809  brcolinear  36824  lineext  36841  brfs  36844  fscgr  36845  linecgr  36846  btwnconn1lem4  36855  btwnconn1lem8  36859  btwnconn1lem11  36862  btwnconn1lem12  36863  segcon2  36870  brsegle  36873  outsideofeq  36895  funray  36905  funline  36907  fvline  36909  linethru  36918  disjeq12dv  37004  prodeq12sdv  37007  itgeq12sdv  37008  cbvitgvw2  37037  cbvitgdavw  37070  cbvitgdavw2  37086  trer  37104  finminlem  37106  ivthALT  37123  filnetlem4  37169  axtco1  37261  axtco1from2  37263  ttcexg  37320  mh-infprim1bi  37334  knoppndvlem21  37398  bj-sepg  37836  bj-elgab  37852  bj-imdirvallem  38101  csboprabg  38253  topdifinffinlem  38270  icoreval  38276  isbasisrelowllem1  38278  isbasisrelowllem2  38279  relowlssretop  38286  pibp19  38337  ptrest  38537  poimirlem1  38539  poimirlem13  38551  poimirlem14  38552  poimirlem22  38560  poimirlem24  38562  poimirlem26  38564  poimirlem27  38565  heicant  38573  mblfinlem3  38577  mblfinlem4  38578  mbfresfi  38584  itg2addnclem3  38591  itg2addnc  38592  itg2gt0cn  38593  areacirclem5  38630  cover2  38649  cover2g  38650  fdc  38679  fdc1  38680  heibor1  38744  bfp  38758  rngosn3  38858  drngoi  38885  isdrngo1  38890  isriscg  38918  isfldidl2  39003  raldmqseu  39297  eldmxrncnvepres  39366  brressn  39463  islshpat  40074  lcvbr  40078  lshpsmreu  40166  ldual1dim  40223  cvrval  40326  cvrnbtwn3  40333  iscvlat2N  40381  ishlat3N  40411  hlrelat5N  40458  3dim0  40514  llnexatN  40578  islpln5  40592  islvol5  40636  pmapjat1  40910  ltrnu  41178  cdleme02N  41279  cdlemg33b  41764  cdlemg33c  41765  dvhb1dimN  42043  dibelval3  42204  dibopelval3  42205  dib1dim  42222  dibglbN  42223  diblsmopel  42228  dicval  42233  dicopelval  42234  dicelval3  42237  dicelval1sta  42244  dihopelvalcpre  42305  dih1dimatlem  42386  dihpN  42393  dihjatcclem4  42478  lpolsetN  42539  mapdpglem3  42732  hdmapglem7a  42984  sticksstones23  43219  exfinfldd  43253  fimgmcyclem  43597  fimgmcyc  43598  fsuppind  43618  fsuppssindlem2  43620  prjspeclsp  43640  mrefg2  43717  mzpclval  43735  eldiophb  43767  eldioph2lem1  43770  eldioph3  43776  lzenom  43780  diophin  43782  eldiophss  43784  diophrex  43785  eq0rabdioph  43786  pellexlem3  43837  elpell1qr  43853  elpell14qr  43855  elpell1234qr  43857  jm2.27  44014  rmydioph  44020  expdiophlem1  44027  expdioph  44029  pw2f1ocnv  44043  hbtlem1  44124  hbtlem7  44126  dgraalem  44146  dgraaub  44149  dflim7  44274  omabs2  44333  tfsconcatfv2  44341  tfsconcat0i  44346  nadd1suc  44393  ifpbi2  44467  inintabd  44579  cnvcnvintabd  44599  cnvintabd  44602  clcnvlem  44622  iunrelexpmin1  44707  uneqsn  45024  k0004lem2  45147  mnuprdlem1  45255  mnuprdlem2  45256  binomcxplemnotnn0  45339  2sbc6g  45398  2sbc5g  45399  iotasbc  45402  dropab1  45429  dropab2  45430  relpeq5  45937  modelaxreplem3  45969  omssaxinf2  45977  brpermmodel  45992  permaxinf2lem  46001  cbvmpo1  46112  r19.28zf  46173  disjinfi  46206  dmrelrnrel  46238  mullimc  46627  mullimcf  46634  limsuppnfd  46711  limsuppnf  46720  limsupre2  46734  limsupre2mpt  46739  limsupre3  46742  limsupre3mpt  46743  limsupre3uzlem  46744  fourierdlem42  47158  fourierdlem48  47163  fourierdlem50  47165  fourierdlem51  47166  fourierdlem54  47169  fourierdlem86  47201  ovnval2  47554  ovnsubaddlem1  47579  hoiqssbl  47634  vonicclem2  47693  f1cof1b  48146  f1ocof1ob2  48151  funressnbrafv2  48313  dfatdmfcoafv2  48323  2ffzoeq  48397  fundcmpsurbijinj  48491  ichreuopeq  48554  prproropf1olem4  48587  prprspr2  48599  prprsprreu  48600  prprreueq  48601  reuopreuprim  48607  nprmmul3  48610  isubgrgrim  49026  grtriprop  49038  isgrtri  49040  opgpgvtx  49152  pgnbgreunbgrlem1  49210  pgnbgreunbgrlem4  49216  grlimedgnedg  49228  rngcsectALTV  49371  rngcinvALTV  49372  ringcsectALTV  49405  ringcinvALTV  49406  lmod1  49603  elbigo2  49663  rrx2vlinest  49852  eloprab1st2nd  49977  i0oii  50027  io1ii  50028  lubeldm2d  50065  glbeldm2d  50066  sectpropdlem  50143  invpropdlem  50145  isopropdlem  50147  uppropd  50288  functhinc  50555  fullthinc  50557