Theorem anbi1d 629

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 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 577	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  anbi12d  630  anbi1  631  pm5.71  1025  cador  1608  drsb1  2493  eleq1w  2815  eleq1d  2817  clelab  2878  rexeqfOLD  3350  rmoeq1OLD  3415  reueq1OLD  3416  rmoeq1f  3419  rabeq  3445  rabeqd  3459  rabeqf  3465  rabeqiOLD  3470  cgsex4gOLD  3521  vtocl2gaf  3568  vtocl4ga  3573  alexeqg  3639  elrabiOLD  3678  reu2eqd  3732  sbc2or  3786  sbc5ALT  3806  rexss  4055  psstr  4104  difin2  4291  r19.28z  4497  dfif6  4531  rexreusng  4683  reurexprg  4708  rabsnifsb  4726  ssunsn2  4830  preq12bg  4854  opeq1  4873  eluni  4911  csbuni  4940  unissb  4943  disjxun  5146  unopab  5230  mpteq12da  5233  mpteq12f  5236  mpteq12dva  5237  dftr2c  5268  axrep1  5286  axreplem  5287  zfrepclf  5294  axsepgfromrep  5297  axsepg  5300  zfauscl  5301  reusv2lem4  5399  rabxfrd  5415  opthg  5477  otthg  5485  copsexgw  5490  copsexg  5491  opeqsng  5503  euotd  5513  elopabw  5526  pocl  5595  poclOLD  5596  xpeq1  5690  elxpi  5698  vtoclr  5739  opbrop  5773  dmopab2rex  5917  resopab2  6036  dflim2  6421  dffun2  6553  fun11  6622  feq2  6699  f1eq2  6783  f1eq3  6784  foeq2  6802  brprcneu  6881  brprcneuALT  6882  ssimaexg  6977  dmfco  6987  fndmdif  7043  respreima  7067  isoeq5  7321  isoini  7338  isopolem  7345  f1oiso  7351  f1oiso2  7352  imaeqsexv  7363  riotaeqdv  7369  oprabidw  7443  oprabid  7444  oprabv  7472  mpoeq123  7484  mpoeq123dva  7486  0mpo0  7495  eloprabga  7519  eloprabgaOLD  7520  resoprab  7529  resoprab2  7530  elrnmpores  7549  ov  7555  ov3  7574  ov6g  7575  ovg  7576  imaeqexov  7649  caoftrn  7712  uniuni  7753  limuni3  7845  elxp4  7917  elxp5  7918  opabex3d  7956  opabex3rd  7957  opabex3  7958  releldmdifi  8035  opiota  8049  eloprabi  8053  mptmpoopabbrd  8071  mptmpoopabbrdOLD  8072  mptmpoopabbrdOLDOLD  8074  cnvf1o  8102  frxp  8117  xporderlem  8118  poxp  8119  fnwelem  8122  poxp2  8134  xpord3pred  8143  poseq  8149  soseq  8150  suppimacnv  8164  rexsupp  8172  mpocurryd  8260  smoel2  8369  omeu  8591  oeeui  8608  omabs  8656  omopth  8667  eldifsucnn  8669  qliftel  8800  brecop  8810  eroveu  8812  erov  8814  ecopovtrn  8820  ixpsnf1o  8938  dom2lem  8994  mapsnend  9042  xpsnen  9061  xpassen  9072  pw2f1olem  9082  xpf1o  9145  unxpdom  9259  domunfican  9326  preleqALT  9618  zfinf  9640  cantnfs  9667  brttrcl  9714  ttrclselem2  9727  tcvalg  9739  r0weon  10013  fseqenlem1  10025  acni2  10047  aceq1  10118  aceq0  10119  dfac2a  10130  dfac12lem2  10145  cardcf  10253  cfeq0  10257  cfsuc  10258  cff1  10259  cfss  10266  isf32lem5  10358  fin1a2lem6  10406  zfac  10461  brdom7disj  10532  brdom6disj  10533  axrepnd  10595  axunndlem1  10596  axinfnd  10607  axacndlem5  10612  axacnd  10613  zfcndrep  10615  zfcndinf  10619  zfcndac  10620  pwfseqlem4a  10662  pwfseqlem4  10663  gruina  10819  grothomex  10830  ordpipq  10943  elnpi  10989  genpass  11010  ltprord  11031  reclem2pr  11049  reclem3pr  11050  recexpr  11052  addsrmo  11074  mulsrmo  11075  addsrpr  11076  mulsrpr  11077  ltsosr  11095  mulgt0sr  11106  supsr  11113  ltresr  11141  axpre-lttrn  11167  axpre-mulgt0  11169  prime  12650  peano5uzti  12659  rexuz  12889  ltxr  13102  qbtwnre  13185  xmulneg1  13255  supxr2  13300  ixxval  13339  fzval  13493  preduz  13630  nn0opth2  14239  hashbclem  14418  hashf1lem2  14424  eqwrd  14514  pfxeq  14653  wrd2ind  14680  cshwcsh2id  14786  eqwrds3  14919  cleq1lem  14936  rtrclreclem3  15014  rtrclreclem4  15015  relexpindlem  15017  abslt  15268  absle  15269  lenegsq  15274  abs2difabs  15288  ello12  15467  elo12  15478  o1lo1  15488  rlimuni  15501  lo1resb  15515  o1resb  15517  2clim  15523  rlimcn3  15541  climcn2  15544  addcn2  15545  mulcn2  15547  o1of2  15564  sumeq1  15642  fsum2dlem  15723  modfsummod  15747  prodeq1f  15859  fprod2dlem  15931  nndivdvds  16213  divalg2  16355  smupval  16436  gcdval  16444  gcdass  16496  lcmval  16536  lcmass  16558  rpexp  16666  pythagtriplem2  16757  pythagtrip  16774  vdwapun  16914  0ram  16960  ramub1lem2  16967  pwsle  17445  imasleval  17494  ismre  17541  ismri  17582  iscatd2  17632  dfiso2  17726  isssc  17774  funcpropd  17858  fullpropd  17878  fthres2b  17888  fthres2c  17889  setcsect  18046  cat1lem  18053  cat1  18054  prslem  18258  drsdir  18262  posi  18277  tosso  18379  odudlatb  18485  ipoval  18490  ipolt  18495  dirge  18563  gsumpropd2lem  18607  mgmhmpropd  18626  issgrpv  18649  issgrpn0  18650  ismhm0  18715  mhmpropd  18717  mndind  18748  mgmnsgrpex  18851  issubg3  19064  isga  19200  symgfixelq  19346  psgnfval  19413  psgnval  19420  dprdw  19925  subgdmdprd  19949  isrnghm  20336  issubrg  20465  resrhm2b  20496  drngpropd  20541  islmod  20622  lmodlema  20623  lmodprop2d  20682  lsslss  20720  lbspropd  20858  lbsacsbs  20918  znleval  21333  islbs4  21610  islinds3  21612  aspval2  21675  psrbag  21693  pf1ind  22107  mdetunilem4  22350  mdetunilem9  22355  istopg  22630  basis2  22687  tg2  22701  iscld  22764  isnei  22840  isneip  22842  neiptoptop  22868  neiptopnei  22869  neitr  22917  restlp  22920  iscn  22972  cnpval  22973  iscnp  22974  regsep  23071  1stcclb  23181  2ndc1stc  23188  2ndcctbss  23192  2ndcdisj  23193  llyi  23211  nllyi  23212  hausmapdom  23237  locfinnei  23260  comppfsc  23269  elkgen  23273  txbas  23304  txcls  23341  txcnpi  23345  ptpjopn  23349  txdis1cn  23372  txtube  23377  txcmplem1  23378  hausdiag  23382  tx1stc  23387  txkgen  23389  xkococn  23397  elqtop  23434  kqreglem1  23478  elmptrab  23564  isfbas  23566  elflim2  23701  elflim  23708  hauspwpwf1  23724  alexsublem  23781  ghmcnp  23852  qustgplem  23858  tsmssubm  23880  elutop  23971  ustuqtop4  23982  isucn  24016  iscfilu  24026  ispsmet  24043  ismet  24062  isxmet  24063  ismet2  24072  imasdsf1olem  24112  blres  24170  elmopn  24181  mopni  24234  neibl  24243  nrmmetd  24316  ngppropd  24379  elcncf  24642  mulc1cncf  24658  elpi1  24805  isclmp  24857  metcld2  25068  pmltpclem1  25210  itg1climres  25477  itg2val  25491  isibl  25528  itgeq1f  25534  itgresr  25541  iblcn  25561  itgfsum  25589  dvreslem  25671  dvfsumlem2  25793  deg1ldg  25859  vieta1  26075  ulm2  26147  sincosq2sgn  26260  sincosq4sgn  26262  efopn  26417  dvdsflsumcom  26943  fsumvma2  26968  logfac2  26971  dchrptlem1  27018  lgsdchrval  27108  2lgslem1a  27145  pntibndlem3  27346  pntlemi  27358  pntleme  27362  pnt3  27366  sltval  27401  nolt02o  27449  slelttr  27511  nocvxminlem  27530  madebday  27646  sltlpss  27653  addsprop  27713  mulsproplemcbv  27825  mulsproplem1  27826  mulsprop  27840  istrkgld  27992  istrkg2ld  27993  istrkg3ld  27994  axtgsegcon  27997  axtg5seg  27998  axtgpasch  28000  axtgupdim2  28004  legov  28118  islnopp  28272  ishpg  28292  iscgra1  28343  dfcgra2  28363  dfcgrg2  28396  brcgr  28440  brbtwn2  28445  axsegconlem1  28457  axsegcon  28467  axcontlem10  28513  edgssv2  28737  uhgr2edg  28747  isfusgrf1  28859  edgnbusgreu  28906  cplgr3v  28974  vtxdun  29020  upgr2wlk  29207  upgrtrls  29240  upgristrl  29241  upgrf1istrl  29242  2pthnloop  29270  usgr2pth  29303  isclwlke  29316  isclwlkupgr  29317  iswwlksnx  29376  wlknewwlksn  29423  2pthon3v  29479  elwwlks2on  29495  wpthswwlks2on  29497  rusgrnumwwlkl1  29504  rusgrnumwwlkb0  29507  clwwlknp  29572  clwwlkf  29582  erclwwlknsym  29605  erclwwlkntr  29606  clwwlknonwwlknonb  29641  0trl  29657  0spth  29661  0crct  29668  0cycl  29669  upgr4cycl4dv4e  29720  upgriseupth  29742  eupth2lem2  29754  3cyclfrgrrn1  29820  4cycl2vnunb  29825  frgrncvvdeqlem2  29835  frgr2wwlk1  29864  fusgr2wsp2nb  29869  numclwlk1lem1  29904  vciOLD  30096  isvclem  30112  nmoofval  30297  isph  30357  norm3lemt  30687  isch2  30758  cmbr  31119  eigre  31370  eigorth  31373  nmopub  31443  nmfnleub  31460  cvbr  31817  mdbr  31829  dmdbr  31834  chrelat2  31905  mdsymlem2  31939  rexunirn  32014  ifeqeqx  32056  iunrnmptss  32079  funcnvmpt  32174  ressupprn  32194  1stpreima  32210  fpwrelmapffslem  32239  isomnd  32504  archirng  32619  isslmd  32632  slmdlema  32633  urpropd  32663  orngmul  32706  lindflbs  32784  islbs5  32785  lindfpropd  32787  opprqus0g  32893  idlsrgval  32906  ressply1mon1p  32946  ccfldextdgrr  33050  dya2iocuni  33595  omsfval  33606  elcarsg  33617  itgeq12dv  33638  isrrvv  33755  reprinrn  33943  reprdifc  33952  istrkg2d  33991  axtgupdim2ALTV  33993  brafs  33997  bnj956  34100  bnj1146  34115  bnj18eq1  34251  zltp1ne  34412  isacycgr  34449  kur14  34520  pconncn  34528  cnpconn  34534  txpconn  34536  cvmscbv  34562  cvmcov  34567  cvmsi  34569  cvmsval  34570  cvmopnlem  34582  cvmlift2lem10  34616  cvmlift3lem2  34624  cvmlift3lem6  34628  cvmlift3lem7  34629  cvmlift3lem9  34631  cvmlift3  34632  satf0op  34681  sat1el2xp  34683  satffunlem  34705  dmopab3rexdif  34709  mclsssvlem  34866  mclsind  34874  eldm3  35050  opelco3  35065  dfon2lem6  35079  dfon2lem7  35080  dfon2lem8  35081  dfon2  35083  elfuns  35206  brsuccf  35232  brofs  35296  5segofs  35297  brifs  35334  ifscgr  35335  brcolinear  35350  lineext  35367  brfs  35370  fscgr  35371  linecgr  35372  btwnconn1lem4  35381  btwnconn1lem8  35385  btwnconn1lem11  35388  btwnconn1lem12  35389  segcon2  35396  brsegle  35399  outsideofeq  35421  funray  35431  funline  35433  fvline  35435  linethru  35444  gg-dvfsumlem2  35480  trer  35517  finminlem  35519  ivthALT  35536  filnetlem4  35582  knoppndvlem21  35724  bj-zfauscl  36120  bj-elgab  36135  bj-imdirvallem  36377  csboprabg  36527  topdifinffinlem  36544  icoreval  36550  isbasisrelowllem1  36552  isbasisrelowllem2  36553  relowlssretop  36560  pibp19  36611  wl-ax11-lem8  36770  curf  36782  ptrest  36803  poimirlem1  36805  poimirlem13  36817  poimirlem14  36818  poimirlem22  36826  poimirlem24  36828  poimirlem26  36830  poimirlem27  36831  heicant  36839  mblfinlem3  36843  mblfinlem4  36844  mbfresfi  36850  itg2addnclem3  36857  itg2addnc  36858  itg2gt0cn  36859  areacirclem5  36896  cover2  36899  cover2g  36900  fdc  36929  fdc1  36930  heibor1  36994  bfp  37008  rngosn3  37108  drngoi  37135  isdrngo1  37140  isriscg  37168  isfldidl2  37253  brressn  37627  islshpat  38203  lcvbr  38207  lshpsmreu  38295  ldual1dim  38352  cvrval  38455  cvrnbtwn3  38462  iscvlat2N  38510  ishlat3N  38540  hlrelat5N  38588  3dim0  38644  llnexatN  38708  islpln5  38722  islvol5  38766  pmapjat1  39040  ltrnu  39308  cdleme02N  39409  cdlemg33b  39894  cdlemg33c  39895  dvhb1dimN  40173  dibelval3  40334  dibopelval3  40335  dib1dim  40352  dibglbN  40353  diblsmopel  40358  dicval  40363  dicopelval  40364  dicelval3  40367  dicelval1sta  40374  dihopelvalcpre  40435  dih1dimatlem  40516  dihpN  40523  dihjatcclem4  40608  lpolsetN  40669  mapdpglem3  40862  hdmapglem7a  41114  fsuppind  41477  fsuppssindlem2  41479  prjspeclsp  41669  mrefg2  41760  mzpclval  41778  eldiophb  41810  eldioph2lem1  41813  eldioph3  41819  lzenom  41823  diophin  41825  eldiophss  41827  diophrex  41828  eq0rabdioph  41829  pellexlem3  41884  elpell1qr  41900  elpell14qr  41902  elpell1234qr  41904  jm2.27  42062  rmydioph  42068  expdiophlem1  42075  expdioph  42077  pw2f1ocnv  42091  hbtlem1  42180  hbtlem7  42182  dgraalem  42202  dgraaub  42205  dflim7  42338  omabs2  42397  tfsconcatfv2  42405  tfsconcat0i  42410  nadd1suc  42457  ifpbi2  42533  inintabd  42645  cnvcnvintabd  42666  cnvintabd  42669  clcnvlem  42689  iunrelexpmin1  42774  uneqsn  43091  k0004lem2  43214  mnuprdlem1  43346  mnuprdlem2  43347  binomcxplemnotnn0  43430  2sbc6g  43489  2sbc5g  43490  iotasbc  43493  dropab1  43521  dropab2  43522  cbvmpo1  44101  r19.28zf  44167  disjinfi  44202  dmrelrnrel  44236  mullimc  44643  mullimcf  44650  limsuppnfd  44729  limsuppnf  44738  limsupre2  44752  limsupre2mpt  44757  limsupre3  44760  limsupre3mpt  44761  limsupre3uzlem  44762  fourierdlem42  45176  fourierdlem48  45181  fourierdlem50  45183  fourierdlem51  45184  fourierdlem54  45187  fourierdlem86  45219  ovnval2  45572  ovnsubaddlem1  45597  hoiqssbl  45652  vonicclem2  45711  f1cof1b  46096  f1ocof1ob2  46101  funressnbrafv2  46263  dfatdmfcoafv2  46273  2ffzoeq  46347  fundcmpsurbijinj  46389  ichreuopeq  46452  prproropf1olem4  46485  prprspr2  46497  prprsprreu  46498  prprreueq  46499  reuopreuprim  46505  rngcsect  46979  rngcinv  46980  rngcsectALTV  46991  rngcinvALTV  46992  ringcsect  47030  ringcinv  47031  ringcsectALTV  47054  ringcinvALTV  47055  lmod1  47273  elbigo2  47338  rrx2vlinest  47527  i0oii  47652  io1ii  47653  lubeldm2d  47691  glbeldm2d  47692  functhinc  47765  fullthinc  47766