Theorem anbi1d 631

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 578	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  anbi12d  632  anbi1  633  pm5.71  1029  cador  1608  drsb1  2493  eleq1w  2811  eleq1d  2813  clelab  2873  rexeqfOLD  3322  rmoeq1OLD  3380  reueq1OLD  3381  rmoeq1f  3386  rabeq  3411  rabeqbidva  3413  rabeqd  3425  rabeqf  3431  cgsex4gOLD  3486  vtocl2gafOLD  3537  vtocl4gaOLD  3544  alexeqg  3608  reu2eqd  3698  sbc2or  3753  sbc5ALT  3773  rexssOLD  4015  psstr  4060  difin2  4254  r19.28z  4451  dfif6  4481  rabsneq  4598  rexreusng  4633  reurexprg  4658  rabsnifsb  4676  ssunsn2  4781  preq12bg  4807  opeq1  4827  eluni  4864  csbuni  4890  unissb  4893  iuneq12d  4974  disjxun  5093  unopab  5175  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  dftr2c  5205  axrep1  5222  axreplem  5223  zfrepclf  5233  axsepgfromrep  5236  axsepg  5239  zfauscl  5240  reusv2lem4  5343  rabxfrd  5359  opthg  5424  otthg  5432  copsexgw  5437  copsexg  5438  opeqsng  5450  euotd  5460  elopabw  5473  pocl  5539  xpeq1  5637  elxpi  5645  vtoclr  5686  opbrop  5721  dmopab2rex  5864  resopab2  5991  dflim2  6369  dffun2  6496  fun11  6560  feq2  6635  f1eq2  6720  f1eq3  6721  foeq2  6737  brprcneu  6816  brprcneuALT  6817  ssimaexg  6913  dmfco  6923  fndmdif  6980  respreima  7004  isoeq5  7262  isoini  7279  isopolem  7286  f1oiso  7292  f1oiso2  7293  imaeqsexvOLD  7304  riotaeqdv  7311  oprabidw  7384  oprabid  7385  oprabv  7413  mpoeq123  7425  mpoeq123dva  7427  0mpo0  7436  eloprabga  7462  resoprab  7471  resoprab2  7472  elrnmpores  7491  ov  7497  ov3  7516  ov6g  7517  ovg  7518  imaeqexov  7591  caoftrn  7658  uniuni  7702  limuni3  7792  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  releldmdifi  7987  opiota  8001  eloprabi  8005  mptmpoopabbrd  8022  mptmpoopabbrdOLD  8023  cnvf1o  8051  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  8527  omabs  8576  omopth  8587  eldifsucnn  8589  qliftel  8734  brecop  8744  eroveu  8746  erov  8748  ecopovtrn  8754  ixpsnf1o  8872  dom2lem  8924  mapsnend  8968  xpsnen  8985  xpassen  8995  pw2f1olem  9005  xpf1o  9063  unxpdom  9158  domunfican  9230  preleqALT  9532  zfinf  9554  cantnfs  9581  brttrcl  9628  ttrclselem2  9641  tcvalg  9653  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  10507  axunndlem1  10508  axinfnd  10519  axacndlem5  10524  axacnd  10525  zfcndrep  10527  zfcndinf  10531  zfcndac  10532  pwfseqlem4a  10574  pwfseqlem4  10575  gruina  10731  grothomex  10742  ordpipq  10855  elnpi  10901  genpass  10922  ltprord  10943  reclem2pr  10961  reclem3pr  10962  recexpr  10964  addsrmo  10986  mulsrmo  10987  addsrpr  10988  mulsrpr  10989  ltsosr  11007  mulgt0sr  11018  supsr  11025  ltresr  11053  axpre-lttrn  11079  axpre-mulgt0  11081  prime  12576  peano5uzti  12585  rexuz  12818  ltxr  13036  qbtwnre  13120  xmulneg1  13190  supxr2  13235  ixxval  13275  fzval  13431  preduz  13572  nn0opth2  14198  hashbclem  14378  hashf1lem2  14382  eqwrd  14483  pfxeq  14621  wrd2ind  14648  cshwcsh2id  14754  eqwrds3  14887  cleq1lem  14908  rtrclreclem3  14986  rtrclreclem4  14987  relexpindlem  14989  abslt  15241  absle  15242  lenegsq  15247  abs2difabs  15261  ello12  15442  elo12  15453  o1lo1  15463  rlimuni  15476  lo1resb  15490  o1resb  15492  2clim  15498  rlimcn3  15516  climcn2  15519  addcn2  15520  mulcn2  15522  o1of2  15539  sumeq1  15615  fsum2dlem  15696  modfsummod  15720  prodeq1f  15832  prodeq1  15833  fprod2dlem  15906  nndivdvds  16191  divalg2  16335  smupval  16418  gcdval  16426  gcdass  16477  lcmval  16522  lcmass  16544  rpexp  16652  pythagtriplem2  16748  pythagtrip  16765  vdwapun  16905  0ram  16951  ramub1lem2  16958  pwsle  17415  imasleval  17464  ismre  17511  ismri  17556  iscatd2  17606  dfiso2  17698  isssc  17746  funcpropd  17828  fullpropd  17848  fthres2b  17858  fthres2c  17859  setcsect  18015  cat1lem  18022  cat1  18023  prslem  18222  drsdir  18227  posi  18242  tosso  18342  odudlatb  18450  ipoval  18455  ipolt  18460  dirge  18528  gsumpropd2lem  18572  mgmhmpropd  18591  issgrpv  18614  issgrpn0  18615  ismhm0  18683  mhmpropd  18685  mndind  18721  mgmnsgrpex  18824  issubg3  19042  isga  19189  symgfixelq  19331  psgnfval  19398  psgnval  19405  dprdw  19910  subgdmdprd  19934  isomnd  20021  isrnghm  20345  issubrg  20475  resrhm2b  20506  rngcsect  20540  rngcinv  20541  ringcsect  20574  ringcinv  20575  drngpropd  20673  orngmul  20769  islmod  20786  lmodlema  20787  lmodprop2d  20846  lsslss  20883  lbspropd  21022  lbsacsbs  21082  znleval  21480  islbs4  21758  islinds3  21760  aspval2  21824  psrbag  21843  pf1ind  22259  mdetunilem4  22519  mdetunilem9  22524  istopg  22799  basis2  22855  tg2  22869  iscld  22931  isnei  23007  isneip  23009  neiptoptop  23035  neiptopnei  23036  neitr  23084  restlp  23087  iscn  23139  cnpval  23140  iscnp  23141  regsep  23238  1stcclb  23348  2ndc1stc  23355  2ndcctbss  23359  2ndcdisj  23360  llyi  23378  nllyi  23379  hausmapdom  23404  locfinnei  23427  comppfsc  23436  elkgen  23440  txbas  23471  txcls  23508  txcnpi  23512  ptpjopn  23516  txdis1cn  23539  txtube  23544  txcmplem1  23545  hausdiag  23549  tx1stc  23554  txkgen  23556  xkococn  23564  elqtop  23601  kqreglem1  23645  elmptrab  23731  isfbas  23733  elflim2  23868  elflim  23875  hauspwpwf1  23891  alexsublem  23948  ghmcnp  24019  qustgplem  24025  tsmssubm  24047  elutop  24138  ustuqtop4  24149  isucn  24182  iscfilu  24192  ispsmet  24209  ismet  24228  isxmet  24229  ismet2  24238  imasdsf1olem  24278  blres  24336  elmopn  24347  mopni  24397  neibl  24406  nrmmetd  24479  ngppropd  24542  elcncf  24799  mulc1cncf  24815  elpi1  24962  isclmp  25014  metcld2  25224  pmltpclem1  25366  itg1climres  25632  itg2val  25646  isibl  25683  itgeq1f  25689  itgeq1fOLD  25690  itgeq1  25691  cbvitgv  25695  itgresr  25697  iblcn  25717  itgfsum  25745  dvreslem  25827  dvfsumlem2  25950  dvfsumlem2OLD  25951  deg1ldg  26014  vieta1  26237  ulm2  26311  sincosq2sgn  26425  sincosq4sgn  26427  efopn  26584  dvdsflsumcom  27115  fsumvma2  27142  logfac2  27145  dchrptlem1  27192  lgsdchrval  27282  2lgslem1a  27319  pntibndlem3  27520  pntlemi  27532  pntleme  27536  pnt3  27540  sltval  27576  nolt02o  27624  slelttr  27686  nocvxminlem  27707  madebday  27833  sltlpss  27841  addsprop  27907  mulsproplemcbv  28042  mulsproplem1  28043  mulsprop  28057  absslt  28175  eucliddivs  28289  zs12ge0  28379  istrkgld  28423  istrkg2ld  28424  istrkg3ld  28425  axtgsegcon  28428  axtg5seg  28429  axtgpasch  28431  axtgupdim2  28435  legov  28549  islnopp  28703  ishpg  28723  iscgra1  28774  dfcgra2  28794  dfcgrg2  28827  brcgr  28864  brbtwn2  28869  axsegconlem1  28881  axsegcon  28891  axcontlem10  28937  edgssv2  29162  uhgr2edg  29172  isfusgrf1  29284  edgnbusgreu  29331  cplgr3v  29399  vtxdun  29446  upgr2wlk  29631  upgrtrls  29664  upgristrl  29665  upgrf1istrl  29666  dfpth2  29693  2pthnloop  29695  usgr2pth  29728  isclwlke  29741  isclwlkupgr  29742  iswwlksnx  29804  wlknewwlksn  29851  2pthon3v  29907  elwwlks2on  29923  wpthswwlks2on  29925  rusgrnumwwlkl1  29932  rusgrnumwwlkb0  29935  clwwlknp  30000  clwwlkf  30010  erclwwlknsym  30033  erclwwlkntr  30034  clwwlknonwwlknonb  30069  0trl  30085  0spth  30089  0crct  30096  0cycl  30097  upgr4cycl4dv4e  30148  upgriseupth  30170  eupth2lem2  30182  3cyclfrgrrn1  30248  4cycl2vnunb  30253  frgrncvvdeqlem2  30263  frgr2wwlk1  30292  fusgr2wsp2nb  30297  numclwlk1lem1  30332  vciOLD  30524  isvclem  30540  nmoofval  30725  isph  30785  norm3lemt  31115  isch2  31186  cmbr  31547  eigre  31798  eigorth  31801  nmopub  31871  nmfnleub  31888  cvbr  32245  mdbr  32257  dmdbr  32262  chrelat2  32333  mdsymlem2  32367  rexunirn  32455  ifeqeqx  32505  iunrnmptss  32528  funcnvmpt  32629  fdifsupp  32646  ressupprn  32651  1stpreima  32668  fpwrelmapffslem  32694  archirng  33149  isslmd  33163  slmdlema  33164  urpropd  33191  lindflbs  33335  islbs5  33336  lindfpropd  33338  opprqus0g  33446  idlsrgval  33459  ressply1mon1p  33522  ccfldextdgrr  33658  constrsslem  33727  constrconj  33731  constrlccllem  33739  constrcbvlem  33741  dya2iocuni  34270  omsfval  34281  elcarsg  34292  itgeq12dv  34313  isrrvv  34430  reprinrn  34605  reprdifc  34614  istrkg2d  34653  axtgupdim2ALTV  34655  brafs  34659  bnj956  34762  bnj1146  34777  bnj18eq1  34913  axsepg2  35068  axsepg2ALT  35069  zltp1ne  35102  isacycgr  35137  kur14  35208  pconncn  35216  cnpconn  35222  txpconn  35224  cvmscbv  35250  cvmcov  35255  cvmsi  35257  cvmsval  35258  cvmopnlem  35270  cvmlift2lem10  35304  cvmlift3lem2  35312  cvmlift3lem6  35316  cvmlift3lem7  35317  cvmlift3lem9  35319  cvmlift3  35320  satf0op  35369  sat1el2xp  35371  satffunlem  35393  dmopab3rexdif  35397  mclsssvlem  35554  mclsind  35562  rexxfr3dALT  35631  eldm3  35753  opelco3  35767  dfon2lem6  35781  dfon2lem7  35782  dfon2lem8  35783  dfon2  35785  elfuns  35908  brsuccf  35934  brofs  35998  5segofs  35999  brifs  36036  ifscgr  36037  brcolinear  36052  lineext  36069  brfs  36072  fscgr  36073  linecgr  36074  btwnconn1lem4  36083  btwnconn1lem8  36087  btwnconn1lem11  36090  btwnconn1lem12  36091  segcon2  36098  brsegle  36101  outsideofeq  36123  funray  36133  funline  36135  fvline  36137  linethru  36146  disjeq12dv  36208  prodeq12sdv  36211  itgeq12sdv  36212  cbvitgvw2  36241  cbvitgdavw  36274  cbvitgdavw2  36290  trer  36309  finminlem  36311  ivthALT  36328  filnetlem4  36374  knoppndvlem21  36525  bj-zfauscl  36917  bj-elgab  36932  bj-imdirvallem  37173  csboprabg  37323  topdifinffinlem  37340  icoreval  37346  isbasisrelowllem1  37348  isbasisrelowllem2  37349  relowlssretop  37356  pibp19  37407  wl-ax11-lem8  37585  curf  37597  ptrest  37618  poimirlem1  37620  poimirlem13  37632  poimirlem14  37633  poimirlem22  37641  poimirlem24  37643  poimirlem26  37645  poimirlem27  37646  heicant  37654  mblfinlem3  37658  mblfinlem4  37659  mbfresfi  37665  itg2addnclem3  37672  itg2addnc  37673  itg2gt0cn  37674  areacirclem5  37711  cover2  37714  cover2g  37715  fdc  37744  fdc1  37745  heibor1  37809  bfp  37823  rngosn3  37923  drngoi  37950  isdrngo1  37955  isriscg  37983  isfldidl2  38068  eldmxrncnvepres  38401  brressn  38437  islshpat  39015  lcvbr  39019  lshpsmreu  39107  ldual1dim  39164  cvrval  39267  cvrnbtwn3  39274  iscvlat2N  39322  ishlat3N  39352  hlrelat5N  39400  3dim0  39456  llnexatN  39520  islpln5  39534  islvol5  39578  pmapjat1  39852  ltrnu  40120  cdleme02N  40221  cdlemg33b  40706  cdlemg33c  40707  dvhb1dimN  40985  dibelval3  41146  dibopelval3  41147  dib1dim  41164  dibglbN  41165  diblsmopel  41170  dicval  41175  dicopelval  41176  dicelval3  41179  dicelval1sta  41186  dihopelvalcpre  41247  dih1dimatlem  41328  dihpN  41335  dihjatcclem4  41420  lpolsetN  41481  mapdpglem3  41674  hdmapglem7a  41926  sticksstones23  42162  exfinfldd  42196  fimgmcyclem  42526  fimgmcyc  42527  fsuppind  42583  fsuppssindlem2  42585  prjspeclsp  42605  mrefg2  42700  mzpclval  42718  eldiophb  42750  eldioph2lem1  42753  eldioph3  42759  lzenom  42763  diophin  42765  eldiophss  42767  diophrex  42768  eq0rabdioph  42769  pellexlem3  42824  elpell1qr  42840  elpell14qr  42842  elpell1234qr  42844  jm2.27  43001  rmydioph  43007  expdiophlem1  43014  expdioph  43016  pw2f1ocnv  43030  hbtlem1  43116  hbtlem7  43118  dgraalem  43138  dgraaub  43141  dflim7  43266  omabs2  43325  tfsconcatfv2  43333  tfsconcat0i  43338  nadd1suc  43385  ifpbi2  43460  inintabd  43572  cnvcnvintabd  43593  cnvintabd  43596  clcnvlem  43616  iunrelexpmin1  43701  uneqsn  44018  k0004lem2  44141  mnuprdlem1  44265  mnuprdlem2  44266  binomcxplemnotnn0  44349  2sbc6g  44408  2sbc5g  44409  iotasbc  44412  dropab1  44440  dropab2  44441  relpeq5  44942  modelaxreplem3  44974  omssaxinf2  44982  brpermmodel  44997  permaxinf2lem  45006  cbvmpo1  45096  r19.28zf  45157  disjinfi  45190  dmrelrnrel  45224  mullimc  45617  mullimcf  45624  limsuppnfd  45703  limsuppnf  45712  limsupre2  45726  limsupre2mpt  45731  limsupre3  45734  limsupre3mpt  45735  limsupre3uzlem  45736  fourierdlem42  46150  fourierdlem48  46155  fourierdlem50  46157  fourierdlem51  46158  fourierdlem54  46161  fourierdlem86  46193  ovnval2  46546  ovnsubaddlem1  46571  hoiqssbl  46626  vonicclem2  46685  f1cof1b  47081  f1ocof1ob2  47086  funressnbrafv2  47248  dfatdmfcoafv2  47258  2ffzoeq  47331  fundcmpsurbijinj  47414  ichreuopeq  47477  prproropf1olem4  47510  prprspr2  47522  prprsprreu  47523  prprreueq  47524  reuopreuprim  47530  isubgrgrim  47933  grtriprop  47945  isgrtri  47947  opgpgvtx  48059  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem4  48123  grlimedgnedg  48135  rngcsectALTV  48279  rngcinvALTV  48280  ringcsectALTV  48313  ringcinvALTV  48314  lmod1  48497  elbigo2  48557  rrx2vlinest  48746  eloprab1st2nd  48872  i0oii  48924  io1ii  48925  lubeldm2d  48962  glbeldm2d  48963  sectpropdlem  49041  invpropdlem  49043  isopropdlem  49045  uppropd  49186  functhinc  49453  fullthinc  49455