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  2529  eleq1w  2848  eleq1d  2850  clelab  2909  rmoeq1f  3408  rabeq  3432  rabeqbidva  3434  rabeqd  3446  rabeqf  3452  alexeqg  3612  reu2eqd  3701  sbc2or  3755  sbc5ALT  3775  rexssOLD  4014  psstr  4063  difin2  4254  r19.28z  4465  dfif6  4492  rabsneq  4610  rexreusng  4647  reurexprg  4672  rabsnifsb  4690  ssunsn2  4795  preq12bg  4820  opeq1  4840  eluni  4877  csbuni  4905  unissb  4908  iuneq12d  4988  disjxun  5109  unopab  5193  mpteq12da  5196  mpteq12f  5198  mpteq12dva  5199  dftr2c  5223  axrep1  5241  axreplem  5242  zfrepclf  5254  axsepgfromrep  5257  axsepg  5260  sepg  5261  zfausclOLD  5263  reusv2lem4  5374  rabxfrd  5390  opthg  5461  otthg  5469  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  opeqsng  5488  euotd  5498  elopabw  5512  pocl  5579  xpeq1  5677  elxpi  5685  vtoclr  5726  opbrop  5761  dmopab2rex  5909  resopab2  6040  rnco  6255  dflim2  6423  dffun2  6550  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  7328  isoini  7345  isopolem  7352  f1oiso  7358  f1oiso2  7359  riotaeqdv  7377  oprabidw  7450  oprabid  7451  oprabv  7479  mpoeq123  7491  mpoeq123dva  7493  0mpo0  7502  eloprabga  7528  resoprab  7537  resoprab2  7538  elrnmpores  7557  ov  7563  ov3  7582  ov6g  7583  ovg  7584  imaeqexov  7658  caoftrn  7725  uniuni  7767  limuni3  7854  elxp4  7925  elxp5  7926  opabex3d  7968  opabex3rd  7969  opabex3  7970  releldmdifi  8048  opiota  8062  eloprabi  8066  mptmpoopabbrd  8084  cnvf1o  8112  frxp  8128  xporderlem  8129  poxp  8130  fnwelem  8133  poxp2  8145  xpord3pred  8154  poseq  8160  soseq  8161  suppimacnv  8176  rexsupp  8184  mpocurryd  8271  smoel2  8356  omeu  8576  oeeui  8594  omabs  8643  omopth  8654  eldifsucnn  8656  qliftel  8804  brecop  8814  eroveu  8816  erov  8818  ecopovtrn  8824  ixpsnf1o  8942  dom2lem  8995  mapsnend  9040  xpsnen  9056  xpassen  9066  pw2f1olem  9076  xpf1o  9134  unxpdom  9226  domunfican  9288  preleqALT  9593  zfinf  9615  cantnfs  9642  brttrcl  9689  ttrclselem2  9702  tcvalg  9712  r0weon  10012  fseqenlem1  10024  acni2  10046  aceq1  10117  aceq0  10118  dfac5lem4  10126  dfac2a  10129  dfac12lem2  10144  cardcf  10250  cfeq0  10255  cfsuc  10256  cff1  10257  cfss  10264  isf32lem5  10356  fin1a2lem6  10404  zfac  10459  brdom7disj  10530  brdom6disj  10531  axrepnd  10596  axunndlem1  10597  axinfnd  10608  axacndlem5  10613  axacnd  10614  zfcndrep  10616  zfcndinf  10620  zfcndac  10621  pwfseqlem4a  10663  pwfseqlem4  10664  gruina  10820  grothomex  10831  ordpipq  10944  elnpi  10990  genpass  11011  ltprord  11032  reclem2pr  11050  reclem3pr  11051  recexpr  11053  addsrmo  11075  mulsrmo  11076  addsrpr  11077  mulsrpr  11078  ltsosr  11096  mulgt0sr  11107  supsr  11114  ltresr  11142  axpre-lttrn  11168  axpre-mulgt0  11170  prime  12695  peano5uzti  12704  rexuz  12940  ltxr  13158  qbtwnre  13243  xmulneg1  13313  supxr2  13358  ixxval  13398  fzval  13555  preduz  13697  nn0opth2  14328  hashbclem  14509  hashf1lem2  14513  eqwrd  14614  pfxeq  14757  wrd2ind  14784  cshwcsh2id  14891  eqwrds3  15024  cleq1lem  15045  rtrclreclem3  15123  rtrclreclem4  15124  relexpindlem  15126  abslt  15392  absle  15393  lenegsq  15398  abs2difabs  15412  ello12  15593  elo12  15604  o1lo1  15614  rlimuni  15627  lo1resb  15641  o1resb  15643  2clim  15649  rlimcn3  15667  climcn2  15670  addcn2  15671  mulcn2  15673  o1of2  15690  sumeq1  15766  fsum2dlem  15846  modfsummod  15871  prodeq1f  15985  prodeq1  15986  fprod2dlem  16059  nndivdvds  16343  divalg2  16487  smupval  16570  gcdval  16578  gcdass  16629  lcmval  16674  lcmass  16696  rpexp  16805  pythagtriplem2  16901  pythagtrip  16918  vdwapun  17058  0ram  17104  ramub1lem2  17111  pwsle  17570  imasleval  17619  ismre  17666  ismri  17711  iscatd2  17761  dfiso2  17853  isssc  17901  funcpropd  17983  fullpropd  18003  fthres2b  18013  fthres2c  18014  setcsect  18170  cat1lem  18177  cat1  18178  prslem  18377  drsdir  18382  posi  18397  tosso  18497  odudlatb  18605  ipoval  18610  ipolt  18615  dirge  18683  mgmidpfod  18762  gsumpropd2lem  18771  mgmhmpropd  18790  issgrpv  18813  issgrpn0  18814  ismhm0  18887  mhmpropd  18889  mndind  18926  mgmnsgrpex  19032  issubg3  19257  isga  19407  symgfixelq  19549  psgnfval  19616  psgnval  19623  dprdw  20128  subgdmdprd  20152  isomnd  20239  isrnghm  20571  issubrg  20722  resrhm2b  20753  rngcsect  20787  rngcinv  20788  ringcsect  20821  ringcinv  20822  drngpropd  20925  orngmul  21020  islmod  21037  lmodlema  21038  lmodprop2d  21097  lsslss  21134  lbspropd  21272  lbsacsbs  21332  isfieldidl2  21439  znleval  21756  islbs4  22034  islinds3  22036  aspval2  22100  psrbag  22119  pf1ind  22567  mdetunilem4  22824  mdetunilem9  22829  istopg  23104  basis2  23160  tg2  23174  iscld  23236  isnei  23312  isneip  23314  neiptoptop  23340  neiptopnei  23341  neitr  23389  restlp  23392  iscn  23444  cnpval  23445  iscnp  23446  regsep  23543  1stcclb  23653  2ndc1stc  23660  2ndcctbss  23665  2ndcdisj  23666  llyi  23684  nllyi  23685  hausmapdom  23710  locfinnei  23733  comppfsc  23742  elkgen  23746  txbas  23777  txcls  23814  txcnpi  23818  ptpjopn  23822  txdis1cn  23845  txtube  23850  txcmplem1  23851  hausdiag  23855  tx1stc  23860  txkgen  23862  xkococn  23870  elqtop  23907  kqreglem1  23951  elmptrab  24037  isfbas  24039  elflim2  24174  elflim  24181  hauspwpwf1  24197  alexsublem  24254  ghmcnp  24325  qustgplem  24331  tsmssubm  24353  elutop  24443  ustuqtop4  24454  isucn  24487  iscfilu  24497  ispsmet  24514  ismet  24533  isxmet  24534  ismet2  24543  imasdsf1olem  24583  blres  24641  elmopn  24652  mopni  24702  neibl  24711  nrmmetd  24784  ngppropd  24847  elcncf  25101  mulc1cncf  25117  elpi1  25257  isclmp  25309  metcld2  25519  pmltpclem1  25660  itg1climres  25926  itg2val  25940  isibl  25977  itgeq1f  25983  itgeq1fOLD  25984  itgeq1  25985  cbvitgv  25989  itgresr  25991  iblcn  26011  itgfsum  26039  dvreslem  26121  dvfsumlem2  26239  deg1ldg  26302  vieta1  26526  ulm2  26601  sincosq2sgn  26717  sincosq4sgn  26719  efopn  26876  dvdsflsumcom  27405  fsumvma2  27431  logfac2  27434  dchrptlem1  27481  lgsdchrval  27571  2lgslem1a  27608  pntibndlem3  27809  pntlemi  27821  pntleme  27825  pnt3  27829  ltsval  27864  nolt02o  27912  leltstr  27978  nocvxminlem  28000  madebday  28146  ltslpss  28154  addsprop  28222  mulsproplemcbv  28361  mulsproplem1  28362  mulsprop  28376  abslts  28495  eucliddivs  28622  bdayfinbndlem2  28714  z12sge0  28729  istrkgld  28781  istrkg2ld  28782  istrkg3ld  28783  axtgsegcon  28786  axtg5seg  28787  axtgpasch  28789  axtgupdim2  28793  legov  28907  islnopp  29073  ishpg  29094  iscgra1  29174  dfcgra2  29194  dfcgrg2  29237  brprlng  29245  brcgr  29307  brbtwn2  29312  axsegconlem1  29324  axsegcon  29334  axcontlem10  29380  edgssv2  29608  uhgr2edg  29618  isfusgrf1  29730  edgnbusgreu  29777  cplgr3v  29845  vtxdun  29891  upgr2wlk  30076  upgrtrls  30113  upgristrl  30114  upgrf1istrl  30115  dfpth2  30143  2pthnloop  30146  usgr2pth  30179  isclwlke  30193  isclwlkupgr  30194  iswwlksnx  30258  wlknewwlksn  30305  2pthon3v  30361  elwwlks2on  30379  wpthswwlks2on  30382  rusgrnumwwlkl1  30389  rusgrnumwwlkb0  30392  clwwlknp  30457  clwwlkf  30467  erclwwlknsym  30490  erclwwlkntr  30491  clwwlknonwwlknonb  30526  0trl  30542  0spth  30546  0crct  30553  0cycl  30554  upgr4cycl4dv4e  30609  upgriseupth  30631  eupth2lem2  30643  3cyclfrgrrn1  30709  4cycl2vnunb  30714  frgrncvvdeqlem2  30724  frgr2wwlk1  30753  fusgr2wsp2nb  30758  numclwlk1lem1  30793  vciOLD  30986  isvclem  31002  nmoofval  31187  isph  31247  norm3lemt  31577  isch2  31648  cmbr  32009  eigre  32260  eigorth  32263  nmopub  32333  nmfnleub  32350  cvbr  32707  mdbr  32719  dmdbr  32724  chrelat2  32795  mdsymlem2  32829  rexunirn  32911  ifeqeqx  32961  iunrnmptss  32983  fdifsupp  33103  ressupprn  33108  1stpreima  33125  fpwrelmapffslem  33149  archirng  33574  isslmd  33588  slmdlema  33589  urpropd  33616  lindflbs  33758  islbs5  33759  lindfpropd  33761  opprqus0g  33838  idlsrgval  33859  ressply1mon1p  33924  ccfldextdgrr  34128  constrsslem  34197  constrconj  34201  constrlccllem  34209  constrcbvlem  34211  dya2iocuni  34740  omsfval  34751  elcarsg  34762  itgeq12dv  34783  isrrvv  34900  reprinrn  35072  reprdifc  35081  istrkg2d  35120  axtgupdim2ALTV  35122  brafs  35129  bnj956  35232  bnj1146  35246  bnj18eq1  35382  axsepg2  35612  axsepg3  35613  axsepg3ALT  35614  axsepg4  35615  axsepg5  35616  zltp1ne  35660  isacycgr  35676  kur14  35747  pconncn  35755  cnpconn  35761  txpconn  35763  cvmscbv  35789  cvmcov  35794  cvmsi  35796  cvmsval  35797  cvmopnlem  35809  cvmlift2lem10  35843  cvmlift3lem2  35851  cvmlift3lem6  35855  cvmlift3lem7  35856  cvmlift3lem9  35858  cvmlift3  35859  satf0op  35908  sat1el2xp  35910  satffunlem  35932  dmopab3rexdif  35936  mclsssvlem  36093  mclsind  36101  rexxfr3dALT  36170  eldm3  36292  opelco3  36306  dfon2lem6  36317  dfon2lem7  36318  dfon2lem8  36319  dfon2  36321  elfuns  36444  lemsuccf  36470  brofs  36536  5segofs  36537  brifs  36574  ifscgr  36575  brcolinear  36590  lineext  36607  brfs  36610  fscgr  36611  linecgr  36612  btwnconn1lem4  36621  btwnconn1lem8  36625  btwnconn1lem11  36628  btwnconn1lem12  36629  segcon2  36636  brsegle  36639  outsideofeq  36661  funray  36671  funline  36673  fvline  36675  linethru  36684  disjeq12dv  36786  prodeq12sdv  36789  itgeq12sdv  36790  cbvitgvw2  36819  cbvitgdavw  36852  cbvitgdavw2  36868  trer  36886  finminlem  36888  ivthALT  36905  filnetlem4  36951  axtco1  37043  axtco1from2  37045  ttcexg  37102  mh-infprim1bi  37116  knoppndvlem21  37180  bj-sepg  37618  bj-elgab  37634  bj-imdirvallem  37883  csboprabg  38035  topdifinffinlem  38052  icoreval  38058  isbasisrelowllem1  38060  isbasisrelowllem2  38061  relowlssretop  38068  pibp19  38119  curf  38308  ptrest  38329  poimirlem1  38331  poimirlem13  38343  poimirlem14  38344  poimirlem22  38352  poimirlem24  38354  poimirlem26  38356  poimirlem27  38357  heicant  38365  mblfinlem3  38369  mblfinlem4  38370  mbfresfi  38376  itg2addnclem3  38383  itg2addnc  38384  itg2gt0cn  38385  areacirclem5  38422  cover2  38426  cover2g  38427  fdc  38456  fdc1  38457  heibor1  38521  bfp  38535  rngosn3  38635  drngoi  38662  isdrngo1  38667  isriscg  38695  isfldidl2  38780  raldmqseu  39074  eldmxrncnvepres  39143  brressn  39240  islshpat  39851  lcvbr  39855  lshpsmreu  39943  ldual1dim  40000  cvrval  40103  cvrnbtwn3  40110  iscvlat2N  40158  ishlat3N  40188  hlrelat5N  40235  3dim0  40291  llnexatN  40355  islpln5  40369  islvol5  40413  pmapjat1  40687  ltrnu  40955  cdleme02N  41056  cdlemg33b  41541  cdlemg33c  41542  dvhb1dimN  41820  dibelval3  41981  dibopelval3  41982  dib1dim  41999  dibglbN  42000  diblsmopel  42005  dicval  42010  dicopelval  42011  dicelval3  42014  dicelval1sta  42021  dihopelvalcpre  42082  dih1dimatlem  42163  dihpN  42170  dihjatcclem4  42255  lpolsetN  42316  mapdpglem3  42509  hdmapglem7a  42761  sticksstones23  42996  exfinfldd  43030  fimgmcyclem  43361  fimgmcyc  43362  fsuppind  43382  fsuppssindlem2  43384  prjspeclsp  43404  mrefg2  43498  mzpclval  43516  eldiophb  43548  eldioph2lem1  43551  eldioph3  43557  lzenom  43561  diophin  43563  eldiophss  43565  diophrex  43566  eq0rabdioph  43567  pellexlem3  43618  elpell1qr  43634  elpell14qr  43636  elpell1234qr  43638  jm2.27  43795  rmydioph  43801  expdiophlem1  43808  expdioph  43810  pw2f1ocnv  43824  hbtlem1  43910  hbtlem7  43912  dgraalem  43932  dgraaub  43935  dflim7  44060  omabs2  44119  tfsconcatfv2  44127  tfsconcat0i  44132  nadd1suc  44179  ifpbi2  44253  inintabd  44365  cnvcnvintabd  44386  cnvintabd  44389  clcnvlem  44409  iunrelexpmin1  44494  uneqsn  44811  k0004lem2  44934  mnuprdlem1  45042  mnuprdlem2  45043  binomcxplemnotnn0  45126  2sbc6g  45185  2sbc5g  45186  iotasbc  45189  dropab1  45216  dropab2  45217  relpeq5  45717  modelaxreplem3  45749  omssaxinf2  45757  brpermmodel  45772  permaxinf2lem  45781  cbvmpo1  45876  r19.28zf  45937  disjinfi  45970  dmrelrnrel  46002  mullimc  46392  mullimcf  46399  limsuppnfd  46476  limsuppnf  46485  limsupre2  46499  limsupre2mpt  46504  limsupre3  46507  limsupre3mpt  46508  limsupre3uzlem  46509  fourierdlem42  46923  fourierdlem48  46928  fourierdlem50  46930  fourierdlem51  46931  fourierdlem54  46934  fourierdlem86  46966  ovnval2  47319  ovnsubaddlem1  47344  hoiqssbl  47399  vonicclem2  47458  f1cof1b  47874  f1ocof1ob2  47879  funressnbrafv2  48041  dfatdmfcoafv2  48051  2ffzoeq  48125  fundcmpsurbijinj  48219  ichreuopeq  48282  prproropf1olem4  48315  prprspr2  48327  prprsprreu  48328  prprreueq  48329  reuopreuprim  48335  nprmmul3  48338  isubgrgrim  48754  grtriprop  48766  isgrtri  48768  opgpgvtx  48880  pgnbgreunbgrlem1  48938  pgnbgreunbgrlem4  48944  grlimedgnedg  48956  rngcsectALTV  49099  rngcinvALTV  49100  ringcsectALTV  49133  ringcinvALTV  49134  lmod1  49331  elbigo2  49391  rrx2vlinest  49580  eloprab1st2nd  49705  i0oii  49757  io1ii  49758  lubeldm2d  49795  glbeldm2d  49796  sectpropdlem  49873  invpropdlem  49875  isopropdlem  49877  uppropd  50018  functhinc  50285  fullthinc  50287