Theorem anbi1d 637

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 583	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:  anbi12d  638  anbi1  639  pm5.71  1035  cador  1615  drsb1  2503  eleq1w  2822  eleq1d  2824  clelab  2883  rmoeq1f  3381  rabeq  3405  rabeqbidva  3407  rabeqd  3419  rabeqf  3425  alexeqg  3589  reu2eqd  3677  sbc2or  3732  sbc5ALT  3752  rexssOLD  3990  psstr  4038  difin2  4229  r19.28z  4430  dfif6  4457  rabsneq  4574  rexreusng  4611  reurexprg  4636  rabsnifsb  4654  ssunsn2  4758  preq12bg  4784  opeq1  4804  eluni  4841  csbuni  4868  unissb  4871  iuneq12d  4951  disjxun  5070  unopab  5152  mpteq12da  5155  mpteq12f  5157  mpteq12dva  5158  dftr2c  5182  axrep1  5200  axreplem  5201  zfrepclf  5213  axsepgfromrep  5216  axsepg  5219  zfauscl  5220  reusv2lem4  5330  rabxfrd  5346  opthg  5417  otthg  5425  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  opeqsng  5444  euotd  5454  elopabw  5468  pocl  5534  xpeq1  5632  elxpi  5640  vtoclr  5681  opbrop  5716  dmopab2rex  5859  resopab2  5988  rnco  6203  dflim2  6368  dffun2  6495  fun11  6559  feq2  6634  f1eq2  6719  f1eq3  6720  foeq2  6736  brprcneu  6817  brprcneuALT  6818  ssimaexg  6913  dmfco  6923  funcnvmpt  6937  fndmdif  6983  respreima  7007  isoeq5  7265  isoini  7282  isopolem  7289  f1oiso  7295  f1oiso2  7296  imaeqsexvOLD  7307  riotaeqdv  7314  oprabidw  7387  oprabid  7388  oprabv  7416  mpoeq123  7428  mpoeq123dva  7430  0mpo0  7439  eloprabga  7465  resoprab  7474  resoprab2  7475  elrnmpores  7494  ov  7500  ov3  7519  ov6g  7520  ovg  7521  imaeqexov  7594  caoftrn  7661  uniuni  7705  limuni3  7792  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  releldmdifi  7987  opiota  8001  eloprabi  8005  mptmpoopabbrd  8022  cnvf1o  8050  frxp  8066  xporderlem  8067  poxp  8068  fnwelem  8071  poxp2  8083  xpord3pred  8092  poseq  8098  soseq  8099  suppimacnv  8114  rexsupp  8122  mpocurryd  8209  smoel2  8293  omeu  8510  oeeui  8528  omabs  8577  omopth  8588  eldifsucnn  8590  qliftel  8737  brecop  8747  eroveu  8749  erov  8751  ecopovtrn  8757  ixpsnf1o  8876  dom2lem  8929  mapsnend  8973  xpsnen  8989  xpassen  8999  pw2f1olem  9009  xpf1o  9067  unxpdom  9159  domunfican  9222  preleqALT  9529  zfinf  9551  cantnfs  9578  brttrcl  9625  ttrclselem2  9638  tcvalg  9648  r0weon  9925  fseqenlem1  9937  acni2  9959  aceq1  10030  aceq0  10031  dfac5lem4  10039  dfac2a  10043  dfac12lem2  10058  cardcf  10165  cfeq0  10169  cfsuc  10170  cff1  10171  cfss  10178  isf32lem5  10270  fin1a2lem6  10318  zfac  10373  brdom7disj  10444  brdom6disj  10445  axrepnd  10508  axunndlem1  10509  axinfnd  10520  axacndlem5  10525  axacnd  10526  zfcndrep  10528  zfcndinf  10532  zfcndac  10533  pwfseqlem4a  10575  pwfseqlem4  10576  gruina  10732  grothomex  10743  ordpipq  10856  elnpi  10902  genpass  10923  ltprord  10944  reclem2pr  10962  reclem3pr  10963  recexpr  10965  addsrmo  10987  mulsrmo  10988  addsrpr  10989  mulsrpr  10990  ltsosr  11008  mulgt0sr  11019  supsr  11026  ltresr  11054  axpre-lttrn  11080  axpre-mulgt0  11082  prime  12601  peano5uzti  12610  rexuz  12839  ltxr  13057  qbtwnre  13142  xmulneg1  13212  supxr2  13257  ixxval  13297  fzval  13454  preduz  13595  nn0opth2  14225  hashbclem  14405  hashf1lem2  14409  eqwrd  14510  pfxeq  14649  wrd2ind  14676  cshwcsh2id  14781  eqwrds3  14914  cleq1lem  14935  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  abslt  15268  absle  15269  lenegsq  15274  abs2difabs  15288  ello12  15469  elo12  15480  o1lo1  15490  rlimuni  15503  lo1resb  15517  o1resb  15519  2clim  15525  rlimcn3  15543  climcn2  15546  addcn2  15547  mulcn2  15549  o1of2  15566  sumeq1  15642  fsum2dlem  15723  modfsummod  15748  prodeq1f  15862  prodeq1  15863  fprod2dlem  15936  nndivdvds  16221  divalg2  16365  smupval  16448  gcdval  16456  gcdass  16507  lcmval  16552  lcmass  16574  rpexp  16683  pythagtriplem2  16779  pythagtrip  16796  vdwapun  16936  0ram  16982  ramub1lem2  16989  pwsle  17447  imasleval  17496  ismre  17543  ismri  17588  iscatd2  17638  dfiso2  17730  isssc  17778  funcpropd  17860  fullpropd  17880  fthres2b  17890  fthres2c  17891  setcsect  18047  cat1lem  18054  cat1  18055  prslem  18254  drsdir  18259  posi  18274  tosso  18374  odudlatb  18482  ipoval  18487  ipolt  18492  dirge  18560  gsumpropd2lem  18638  mgmhmpropd  18657  issgrpv  18680  issgrpn0  18681  ismhm0  18749  mhmpropd  18751  mndind  18787  mgmnsgrpex  18893  issubg3  19111  isga  19257  symgfixelq  19399  psgnfval  19466  psgnval  19473  dprdw  19978  subgdmdprd  20002  isomnd  20089  isrnghm  20412  issubrg  20543  resrhm2b  20574  rngcsect  20608  rngcinv  20609  ringcsect  20642  ringcinv  20643  drngpropd  20741  orngmul  20837  islmod  20854  lmodlema  20855  lmodprop2d  20914  lsslss  20951  lbspropd  21089  lbsacsbs  21149  znleval  21529  islbs4  21807  islinds3  21809  aspval2  21873  psrbag  21892  pf1ind  22341  mdetunilem4  22598  mdetunilem9  22603  istopg  22878  basis2  22934  tg2  22948  iscld  23010  isnei  23086  isneip  23088  neiptoptop  23114  neiptopnei  23115  neitr  23163  restlp  23166  iscn  23218  cnpval  23219  iscnp  23220  regsep  23317  1stcclb  23427  2ndc1stc  23434  2ndcctbss  23438  2ndcdisj  23439  llyi  23457  nllyi  23458  hausmapdom  23483  locfinnei  23506  comppfsc  23515  elkgen  23519  txbas  23550  txcls  23587  txcnpi  23591  ptpjopn  23595  txdis1cn  23618  txtube  23623  txcmplem1  23624  hausdiag  23628  tx1stc  23633  txkgen  23635  xkococn  23643  elqtop  23680  kqreglem1  23724  elmptrab  23810  isfbas  23812  elflim2  23947  elflim  23954  hauspwpwf1  23970  alexsublem  24027  ghmcnp  24098  qustgplem  24104  tsmssubm  24126  elutop  24216  ustuqtop4  24227  isucn  24260  iscfilu  24270  ispsmet  24287  ismet  24306  isxmet  24307  ismet2  24316  imasdsf1olem  24356  blres  24414  elmopn  24425  mopni  24475  neibl  24484  nrmmetd  24557  ngppropd  24620  elcncf  24874  mulc1cncf  24890  elpi1  25030  isclmp  25082  metcld2  25292  pmltpclem1  25433  itg1climres  25699  itg2val  25713  isibl  25750  itgeq1f  25756  itgeq1fOLD  25757  itgeq1  25758  cbvitgv  25762  itgresr  25764  iblcn  25784  itgfsum  25812  dvreslem  25894  dvfsumlem2  26012  deg1ldg  26075  vieta1  26296  ulm2  26368  sincosq2sgn  26481  sincosq4sgn  26483  efopn  26640  dvdsflsumcom  27169  fsumvma2  27195  logfac2  27198  dchrptlem1  27245  lgsdchrval  27335  2lgslem1a  27372  pntibndlem3  27573  pntlemi  27585  pntleme  27589  pnt3  27593  ltsval  27629  nolt02o  27677  leltstr  27743  nocvxminlem  27764  madebday  27910  ltslpss  27918  addsprop  27986  mulsproplemcbv  28125  mulsproplem1  28126  mulsprop  28140  abslts  28259  eucliddivs  28386  bdayfinbndlem2  28478  z12sge0  28493  istrkgld  28545  istrkg2ld  28546  istrkg3ld  28547  axtgsegcon  28550  axtg5seg  28551  axtgpasch  28553  axtgupdim2  28557  legov  28671  islnopp  28825  ishpg  28845  iscgra1  28896  dfcgra2  28916  dfcgrg2  28949  brcgr  28987  brbtwn2  28992  axsegconlem1  29004  axsegcon  29014  axcontlem10  29060  edgssv2  29285  uhgr2edg  29295  isfusgrf1  29407  edgnbusgreu  29454  cplgr3v  29522  vtxdun  29568  upgr2wlk  29753  upgrtrls  29786  upgristrl  29787  upgrf1istrl  29788  dfpth2  29815  2pthnloop  29817  usgr2pth  29850  isclwlke  29863  isclwlkupgr  29864  iswwlksnx  29926  wlknewwlksn  29973  2pthon3v  30029  elwwlks2on  30047  wpthswwlks2on  30050  rusgrnumwwlkl1  30057  rusgrnumwwlkb0  30060  clwwlknp  30125  clwwlkf  30135  erclwwlknsym  30158  erclwwlkntr  30159  clwwlknonwwlknonb  30194  0trl  30210  0spth  30214  0crct  30221  0cycl  30222  upgr4cycl4dv4e  30273  upgriseupth  30295  eupth2lem2  30307  3cyclfrgrrn1  30373  4cycl2vnunb  30378  frgrncvvdeqlem2  30388  frgr2wwlk1  30417  fusgr2wsp2nb  30422  numclwlk1lem1  30457  vciOLD  30650  isvclem  30666  nmoofval  30851  isph  30911  norm3lemt  31241  isch2  31312  cmbr  31673  eigre  31924  eigorth  31927  nmopub  31997  nmfnleub  32014  cvbr  32371  mdbr  32383  dmdbr  32388  chrelat2  32459  mdsymlem2  32493  rexunirn  32579  ifeqeqx  32630  iunrnmptss  32654  fdifsupp  32777  ressupprn  32782  1stpreima  32799  fpwrelmapffslem  32824  archirng  33269  isslmd  33283  slmdlema  33284  urpropd  33312  lindflbs  33462  islbs5  33463  lindfpropd  33465  opprqus0g  33573  idlsrgval  33586  ressply1mon1p  33651  ccfldextdgrr  33856  constrsslem  33925  constrconj  33929  constrlccllem  33937  constrcbvlem  33939  dya2iocuni  34467  omsfval  34478  elcarsg  34489  itgeq12dv  34510  isrrvv  34627  reprinrn  34802  reprdifc  34811  istrkg2d  34850  axtgupdim2ALTV  34852  brafs  34856  bnj956  34959  bnj1146  34973  bnj18eq1  35109  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg4  35324  axsepg5  35325  zltp1ne  35338  isacycgr  35373  kur14  35444  pconncn  35452  cnpconn  35458  txpconn  35460  cvmscbv  35486  cvmcov  35491  cvmsi  35493  cvmsval  35494  cvmopnlem  35506  cvmlift2lem10  35540  cvmlift3lem2  35548  cvmlift3lem6  35552  cvmlift3lem7  35553  cvmlift3lem9  35555  cvmlift3  35556  satf0op  35605  sat1el2xp  35607  satffunlem  35629  dmopab3rexdif  35633  mclsssvlem  35790  mclsind  35798  rexxfr3dALT  35867  eldm3  35989  opelco3  36003  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon2  36018  elfuns  36141  lemsuccf  36167  brofs  36233  5segofs  36234  brifs  36271  ifscgr  36272  brcolinear  36287  lineext  36304  brfs  36307  fscgr  36308  linecgr  36309  btwnconn1lem4  36318  btwnconn1lem8  36322  btwnconn1lem11  36325  btwnconn1lem12  36326  segcon2  36333  brsegle  36336  outsideofeq  36358  funray  36368  funline  36370  fvline  36372  linethru  36381  disjeq12dv  36443  prodeq12sdv  36446  itgeq12sdv  36447  cbvitgvw2  36476  cbvitgdavw  36509  cbvitgdavw2  36525  trer  36544  finminlem  36546  ivthALT  36563  filnetlem4  36609  axtco1  36701  axtco1from2  36703  ttcexg  36760  mh-infprim1bi  36774  knoppndvlem21  36838  bj-zfauscl  37277  bj-elgab  37292  bj-imdirvallem  37540  csboprabg  37692  topdifinffinlem  37709  icoreval  37715  isbasisrelowllem1  37717  isbasisrelowllem2  37718  relowlssretop  37725  pibp19  37776  curf  37965  ptrest  37986  poimirlem1  37988  poimirlem13  38000  poimirlem14  38001  poimirlem22  38009  poimirlem24  38011  poimirlem26  38013  poimirlem27  38014  heicant  38022  mblfinlem3  38026  mblfinlem4  38027  mbfresfi  38033  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  areacirclem5  38079  cover2  38082  cover2g  38083  fdc  38112  fdc1  38113  heibor1  38177  bfp  38191  rngosn3  38291  drngoi  38318  isdrngo1  38323  isriscg  38351  isfldidl2  38436  raldmqseu  38732  eldmxrncnvepres  38801  brressn  38898  islshpat  39509  lcvbr  39513  lshpsmreu  39601  ldual1dim  39658  cvrval  39761  cvrnbtwn3  39768  iscvlat2N  39816  ishlat3N  39846  hlrelat5N  39893  3dim0  39949  llnexatN  40013  islpln5  40027  islvol5  40071  pmapjat1  40345  ltrnu  40613  cdleme02N  40714  cdlemg33b  41199  cdlemg33c  41200  dvhb1dimN  41478  dibelval3  41639  dibopelval3  41640  dib1dim  41657  dibglbN  41658  diblsmopel  41663  dicval  41668  dicopelval  41669  dicelval3  41672  dicelval1sta  41679  dihopelvalcpre  41740  dih1dimatlem  41821  dihpN  41828  dihjatcclem4  41913  lpolsetN  41974  mapdpglem3  42167  hdmapglem7a  42419  sticksstones23  42654  exfinfldd  42688  fimgmcyclem  43019  fimgmcyc  43020  fsuppind  43040  fsuppssindlem2  43042  prjspeclsp  43062  mrefg2  43156  mzpclval  43174  eldiophb  43206  eldioph2lem1  43209  eldioph3  43215  lzenom  43219  diophin  43221  eldiophss  43223  diophrex  43224  eq0rabdioph  43225  pellexlem3  43276  elpell1qr  43292  elpell14qr  43294  elpell1234qr  43296  jm2.27  43453  rmydioph  43459  expdiophlem1  43466  expdioph  43468  pw2f1ocnv  43482  hbtlem1  43568  hbtlem7  43570  dgraalem  43590  dgraaub  43593  dflim7  43718  omabs2  43777  tfsconcatfv2  43785  tfsconcat0i  43790  nadd1suc  43837  ifpbi2  43911  inintabd  44023  cnvcnvintabd  44044  cnvintabd  44047  clcnvlem  44067  iunrelexpmin1  44152  uneqsn  44469  k0004lem2  44592  mnuprdlem1  44716  mnuprdlem2  44717  binomcxplemnotnn0  44800  2sbc6g  44859  2sbc5g  44860  iotasbc  44863  dropab1  44890  dropab2  44891  relpeq5  45392  modelaxreplem3  45424  omssaxinf2  45432  brpermmodel  45447  permaxinf2lem  45456  cbvmpo1  45545  r19.28zf  45606  disjinfi  45639  dmrelrnrel  45671  mullimc  46061  mullimcf  46068  limsuppnfd  46145  limsuppnf  46154  limsupre2  46168  limsupre2mpt  46173  limsupre3  46176  limsupre3mpt  46177  limsupre3uzlem  46178  fourierdlem42  46592  fourierdlem48  46597  fourierdlem50  46599  fourierdlem51  46600  fourierdlem54  46603  fourierdlem86  46635  ovnval2  46988  ovnsubaddlem1  47013  hoiqssbl  47068  vonicclem2  47127  f1cof1b  47540  f1ocof1ob2  47545  funressnbrafv2  47707  dfatdmfcoafv2  47717  2ffzoeq  47791  fundcmpsurbijinj  47885  ichreuopeq  47948  prproropf1olem4  47981  prprspr2  47993  prprsprreu  47994  prprreueq  47995  reuopreuprim  48001  nprmmul3  48004  isubgrgrim  48420  grtriprop  48432  isgrtri  48434  opgpgvtx  48546  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  grlimedgnedg  48622  rngcsectALTV  48766  rngcinvALTV  48767  ringcsectALTV  48800  ringcinvALTV  48801  lmod1  48983  elbigo2  49043  rrx2vlinest  49232  eloprab1st2nd  49358  i0oii  49410  io1ii  49411  lubeldm2d  49448  glbeldm2d  49449  sectpropdlem  49526  invpropdlem  49528  isopropdlem  49530  uppropd  49671  functhinc  49938  fullthinc  49940