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  2527  eleq1w  2847  eleq1d  2849  clelab  2908  rmoeq1f  3406  rabeq  3430  rabeqbidva  3432  rabeqd  3443  rabeqf  3449  alexeqg  3608  reu2eqd  3697  sbc2or  3751  sbc5ALT  3771  psstr  4038  difin2  4249  r19.28z  4461  dfif6  4488  rabsneq  4603  rexreusng  4641  reurexprg  4666  rabsnifsb  4685  ssunsn2  4788  preq12bg  4813  opeq1  4845  eluni  4875  csbuni  4903  unissb  4906  iuneq12d  4985  disjxun  5106  unopab  5191  mpteq12da  5194  mpteq12f  5196  mpteq12dva  5197  dftr2c  5221  axrep1  5239  axreplem  5240  zfrepclf  5250  axsepgfromrep  5253  axsepg  5256  sepg  5257  zfausclOLD  5259  reusv2lem4  5370  rabxfrd  5386  opthg  5453  otthg  5461  copsexgw  5467  copsexgwOLD  5468  copsexg  5469  cotsexgw  5470  opeqsng  5482  euotd  5493  elopabw  5507  pocl  5574  xpeq1  5672  elxpi  5680  vtoclr  5721  opbrop  5757  dmopab2rex  5911  resopab2  6046  rnco  6272  dflim2  6447  dffun2  6576  fun11  6644  feq2  6718  f1eq2  6804  f1eq3  6805  foeq2  6823  brprcneu  6906  brprcneuALT  6907  ssimaexg  7002  dmfco  7012  funcnvmpt  7026  fndmdif  7072  respreima  7097  isoeq5  7360  isoini  7377  isopolem  7384  f1oiso  7390  f1oiso2  7391  riotaeqdv  7409  oprabidw  7482  oprabid  7483  oprabv  7511  mpoeq123  7523  mpoeq123dva  7525  0mpo0  7534  eloprabga  7560  resoprab  7569  resoprab2  7570  elrnmpores  7590  ov  7596  ov3  7615  ov6g  7616  ovg  7617  imaeqexov  7691  mpt3fvd  7720  caoftrn  7766  uniuni  7808  limuni3  7897  elxp4  7968  elxp5  7969  opabex3d  8011  opabex3rd  8012  opabex3  8013  releldmdifi  8091  opiota  8105  eloprabi  8109  mptmpoopabbrd  8129  cnvf1o  8159  frxp  8175  xporderlem  8176  poxp  8177  fnwelem  8180  poxp2  8197  xpord3pred  8206  poseq  8212  soseq  8213  suppimacnv  8229  rexsupp  8237  mpocurryd  8324  smoel2  8409  omeu  8631  oeeui  8649  omabs  8698  omopth  8709  eldifsucnn  8711  qliftel  8859  brecop  8869  eroveu  8871  erov  8873  ecopovtrn  8879  curf  8928  ixpsnf1o  9004  dom2lem  9057  mapsnend  9102  xpsnen  9118  xpassen  9128  pw2f1olem  9138  xpf1o  9196  unxpdom  9288  domunfican  9351  preleqALT  9655  zfinf  9677  cantnfs  9704  brttrcl  9751  ttrclselem2  9764  tcvalg  9774  r0weon  10130  fseqenlem1  10142  acni2  10164  aceq1  10235  aceq0  10236  dfac5lem4  10244  dfac2a  10247  dfac12lem2  10262  cardcf  10368  cfeq0  10373  cfsuc  10374  cff1  10375  cfss  10382  isf32lem5  10474  fin1a2lem6  10522  zfac  10577  brdom7disj  10649  brdom6disj  10650  axrepnd  10718  axunndlem1  10719  axinfnd  10730  axacndlem5  10735  axacnd  10736  zfcndrep  10738  zfcndinf  10742  zfcndac  10743  pwfseqlem4a  10785  pwfseqlem4  10786  gruina  10942  grothomex  10953  ordpipq  11066  elnpi  11112  genpass  11133  ltprord  11154  reclem2pr  11172  reclem3pr  11173  recexpr  11175  addsrmo  11197  mulsrmo  11198  addsrpr  11199  mulsrpr  11200  ltsosr  11218  mulgt0sr  11229  supsr  11236  ltresr  11264  axpre-lttrn  11290  axpre-mulgt0  11292  prime  12820  peano5uzti  12829  rexuz  13065  ltxr  13284  qbtwnre  13369  xmulneg1  13439  supxr2  13484  ixxval  13524  fzval  13681  preduz  13824  nn0opth2  14457  hashbclem  14638  hashf1lem2  14642  eqwrd  14743  pfxeq  14887  wrd2ind  14914  cshwcsh2id  15021  eqwrds3  15157  cleq1lem  15178  rtrclreclem3  15256  rtrclreclem4  15257  relexpindlem  15259  abslt  15525  absle  15526  lenegsq  15531  abs2difabs  15545  ello12  15727  elo12  15738  o1lo1  15748  rlimuni  15761  lo1resb  15775  o1resb  15777  2clim  15783  rlimcn3  15801  climcn2  15804  addcn2  15805  mulcn2  15807  o1of2  15824  sumeq1  15900  fsum2dlem  15980  modfsummod  16005  prodeq1f  16119  prodeq1  16120  fprod2dlem  16191  nndivdvds  16475  divalg2  16619  smupval  16702  gcdval  16710  gcdass  16764  lcmval  16811  lcmass  16833  rpexp  16942  pythagtriplem2  17039  pythagtrip  17056  vdwapun  17196  0ram  17242  ramub1lem2  17249  pwsle  17714  imasleval  17763  ismre  17810  ismri  17855  iscatd2  17905  dfiso2  17997  isssc  18045  funcpropd  18127  fullpropd  18147  fthres2b  18157  fthres2c  18158  setcsect  18314  cat1lem  18321  cat1  18322  prslem  18521  drsdir  18526  posi  18541  tosso  18641  odudlatb  18749  ipoval  18754  ipolt  18759  dirge  18827  mgmidpfod  18907  gsumpropd2lem  18918  mgmhmpropd  18937  issgrpv  18960  issgrpn0  18961  ismhm0  19035  mhmpropd  19037  mndind  19074  mgmnsgrpex  19180  issubg3  19405  isga  19556  symgfixelq  19698  psgnfval  19765  psgnval  19772  dprdw  20277  subgdmdprd  20301  isomnd  20388  isrnghm  20722  issubrg  20874  resrhm2b  20905  rngcsect  20939  rngcinv  20940  ringcsect  20973  ringcinv  20974  drngpropd  21078  orngmul  21173  islmod  21190  lmodlema  21191  lmodprop2d  21250  lsslss  21287  lbspropd  21425  lbsacsbs  21485  isfieldidl2  21592  znleval  21915  islbs4  22193  islinds3  22195  aspval2  22261  psrbag  22280  pf1ind  22728  mdetunilem4  22985  mdetunilem9  22990  istopg  23268  basis2  23324  tg2  23338  iscld  23400  isnei  23476  isneip  23478  neiptoptop  23504  neiptopnei  23505  neitr  23553  restlp  23556  iscn  23608  cnpval  23609  iscnp  23610  regsep  23707  1stcclb  23817  2ndc1stc  23824  2ndcctbss  23829  2ndcdisj  23830  llyi  23848  nllyi  23849  hausmapdom  23874  locfinnei  23897  comppfsc  23906  elkgen  23910  txbas  23941  txcls  23978  txcnpi  23982  ptpjopn  23986  txdis1cn  24009  txtube  24014  txcmplem1  24015  hausdiag  24019  tx1stc  24024  txkgen  24026  xkococn  24034  elqtop  24071  kqreglem1  24115  elmptrab  24201  isfbas  24203  elflim2  24338  elflim  24345  hauspwpwf1  24361  alexsublem  24418  ghmcnp  24489  qustgplem  24495  tsmssubm  24517  elutop  24607  ustuqtop4  24618  isucn  24651  iscfilu  24661  ispsmet  24678  ismet  24697  isxmet  24698  ismet2  24707  imasdsf1olem  24747  blres  24805  elmopn  24816  mopni  24866  neibl  24875  nrmmetd  24948  ngppropd  25011  elcncf  25265  mulc1cncf  25281  elpi1  25421  isclmp  25473  metcld2  25683  pmltpclem1  25824  itg1climres  26090  itg2val  26104  isibl  26141  itgeq1f  26147  itgeq1  26148  cbvitgv  26152  itgresr  26154  iblcn  26174  itgfsum  26202  dvreslem  26284  dvfsumlem2  26402  deg1ldg  26465  vieta1  26690  ulm2  26769  sincosq2sgn  26885  sincosq4sgn  26887  efopn  27043  dvdsflsumcom  27572  fsumvma2  27598  logfac2  27601  dchrptlem1  27648  lgsdchrval  27738  2lgslem1a  27775  pntibndlem3  27976  pntlemi  27988  pntleme  27992  pnt3  27996  ltsval  28061  nolt02o  28109  leltstr  28175  nocvxminlem  28197  madebday  28343  ltslpss  28351  addsprop  28419  mulsproplemcbv  28558  mulsproplem1  28559  mulsprop  28573  abslts  28692  eucliddivs  28819  bdayfinbndlem2  28911  z12sge0  28926  istrkgld  28978  istrkg2ld  28979  istrkg3ld  28980  axtgsegcon  28983  axtg5seg  28984  axtgpasch  28986  axtgupdim2  28990  legov  29105  islnopp  29272  ishpg  29294  iscgra1  29374  dfcgra2  29395  elcgrabasi  29432  dfcgrg2  29465  brprlng  29473  brcgr  29535  brbtwn2  29540  axsegconlem1  29552  axsegcon  29562  axcontlem10  29608  edgssv2  29836  uhgr2edg  29846  isfusgrf1  29958  edgnbusgreu  30005  cplgr3v  30073  vtxdun  30119  upgr2wlk  30304  upgrtrls  30341  upgristrl  30342  upgrf1istrl  30343  dfpth2  30371  2pthnloop  30374  usgr2pth  30407  isclwlke  30421  isclwlkupgr  30422  iswwlksnx  30486  wlknewwlksn  30533  2pthon3v  30589  elwwlks2on  30607  wpthswwlks2on  30610  rusgrnumwwlkl1  30617  rusgrnumwwlkb0  30620  clwwlknp  30685  clwwlkf  30695  erclwwlknsym  30718  erclwwlkntr  30719  clwwlknonwwlknonb  30754  0trl  30770  0spth  30774  0crct  30781  0cycl  30782  isacycgr  30808  upgr4cycl4dv4e  30843  upgriseupth  30865  eupth2lem2  30877  3cyclfrgrrn1  30943  4cycl2vnunb  30948  frgrncvvdeqlem2  30958  frgr2wwlk1  30987  fusgr2wsp2nb  30992  numclwlk1lem1  31027  vciOLD  31220  isvclem  31236  nmoofval  31421  isph  31481  norm3lemt  31811  isch2  31882  cmbr  32243  eigre  32494  eigorth  32497  nmopub  32567  nmfnleub  32584  cvbr  32941  mdbr  32953  dmdbr  32958  chrelat2  33029  mdsymlem2  33063  rexunirn  33187  ifeqeqx  33236  iunrnmptss  33257  fdifsupp  33375  ressupprn  33380  1stpreima  33397  fpwrelmapffslem  33420  archirng  33848  isslmd  33862  slmdlema  33863  urpropd  33890  edomediv  33955  fldedom  33956  ply1edom  33959  lindflbs  34038  islbs5  34039  lindfpropd  34041  opprqus0g  34118  idlsrgval  34139  ressply1mon1p  34203  ccfldextdgrr  34415  constrsslem  34484  constrconj  34488  constrlccllem  34496  constrcbvlem  34498  dya2iocuni  35026  omsfval  35037  elcarsg  35048  itgeq12dv  35069  isrrvv  35186  reprinrn  35358  reprdifc  35367  istrkg2d  35406  axtgupdim2ALTV  35408  brafs  35415  bnj956  35518  bnj1146  35532  bnj18eq1  35668  omeueq  35837  mpofvd  35838  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg4  35952  axsepg5  35953  zltp1ne  36098  kur14  36189  pconncn  36197  cnpconn  36203  txpconn  36205  cvmscbv  36231  cvmcov  36236  cvmsi  36238  cvmsval  36239  cvmopnlem  36251  cvmlift2lem10  36285  cvmlift3lem2  36293  cvmlift3lem6  36297  cvmlift3lem7  36298  cvmlift3lem9  36300  cvmlift3  36301  satf0op  36350  sat1el2xp  36352  satffunlem  36374  dmopab3rexdif  36378  mclsssvlem  36535  mclsind  36543  rexxfr3dALT  36612  elpssmo  36673  eldm3  36741  opelco3  36754  dfon2lem6  36765  dfon2lem7  36766  dfon2lem8  36767  dfon2  36769  elfuns  36892  lemsuccf  36918  brofs  36985  5segofs  36986  brifs  37023  ifscgr  37024  brcolinear  37039  lineext  37056  brfs  37059  fscgr  37060  linecgr  37061  btwnconn1lem4  37070  btwnconn1lem8  37074  btwnconn1lem11  37077  btwnconn1lem12  37078  segcon2  37085  brsegle  37088  outsideofeq  37110  funray  37120  funline  37122  fvline  37124  linethru  37133  disjeq12dv  37219  prodeq12sdv  37222  itgeq12sdv  37223  cbvitgvw2  37252  cbvitgdavw  37285  cbvitgdavw2  37301  trer  37319  finminlem  37321  ivthALT  37338  filnetlem4  37384  axtco1  37476  axtco1from2  37478  ttcexg  37535  mh-infprim1bi  37549  knoppndvlem21  37613  bj-sepg  38051  bj-elgab  38067  bj-imdirvallem  38369  csboprabg  38521  topdifinffinlem  38538  icoreval  38544  isbasisrelowllem1  38546  isbasisrelowllem2  38547  relowlssretop  38554  pibp19  38605  ptrest  38805  poimirlem1  38807  poimirlem13  38819  poimirlem14  38820  poimirlem22  38828  poimirlem24  38830  poimirlem26  38832  poimirlem27  38833  heicant  38841  mblfinlem3  38845  mblfinlem4  38846  mbfresfi  38852  itg2addnclem3  38859  itg2addnc  38860  itg2gt0cn  38861  areacirclem5  38898  cover2  38917  cover2g  38918  fdc  38945  fdc1  38946  heibor1  39010  bfp  39024  rngosn3  39124  drngoi  39151  isdrngo1  39156  isriscg  39184  isfldidl2  39269  raldmqseu  39563  eldmxrncnvepres  39632  brressn  39729  islshpat  40340  lcvbr  40344  lshpsmreu  40432  ldual1dim  40489  cvrval  40592  cvrnbtwn3  40599  iscvlat2N  40647  ishlat3N  40677  hlrelat5N  40724  3dim0  40780  llnexatN  40844  islpln5  40858  islvol5  40902  pmapjat1  41176  ltrnu  41444  cdleme02N  41545  cdlemg33b  42030  cdlemg33c  42031  dvhb1dimN  42309  dibelval3  42470  dibopelval3  42471  dib1dim  42488  dibglbN  42489  diblsmopel  42494  dicval  42499  dicopelval  42500  dicelval3  42503  dicelval1sta  42510  dihopelvalcpre  42571  dih1dimatlem  42652  dihpN  42659  dihjatcclem4  42744  lpolsetN  42805  mapdpglem3  42998  hdmapglem7a  43250  sticksstones23  43485  exfinfldd  43519  fimgmcyclem  43863  fimgmcyc  43864  fsuppind  43884  fsuppssindlem2  43886  prjspeclsp  43906  mrefg2  43984  mzpclval  44002  eldiophb  44034  eldioph2lem1  44037  eldioph3  44043  lzenom  44047  diophin  44049  eldiophss  44051  diophrex  44052  eq0rabdioph  44053  pellexlem3  44104  elpell1qr  44120  elpell14qr  44122  elpell1234qr  44124  jm2.27  44281  rmydioph  44287  expdiophlem1  44294  expdioph  44296  pw2f1ocnv  44310  hbtlem1  44390  hbtlem7  44392  dgraalem  44412  dgraaub  44415  dflim7  44536  omabs2  44595  tfsconcatfv2  44603  tfsconcat0i  44608  nadd1suc  44655  ifpbi2  44729  inintabd  44841  cnvcnvintabd  44861  cnvintabd  44864  clcnvlem  44884  iunrelexpmin1  44969  uneqsn  45286  k0004lem2  45409  mnuprdlem1  45517  mnuprdlem2  45518  binomcxplemnotnn0  45601  2sbc6g  45660  2sbc5g  45661  iotasbc  45663  dropab1  45690  dropab2  45691  relpeq5  46202  modelaxreplem3  46234  omssaxinf2  46242  brpermmodel  46257  permaxinf2lem  46266  cbvmpo1  46386  r19.28zf  46447  disjinfi  46480  dmrelrnrel  46512  mullimc  46901  mullimcf  46908  limsuppnfd  46985  limsuppnf  46994  limsupre2  47008  limsupre2mpt  47013  limsupre3  47016  limsupre3mpt  47017  limsupre3uzlem  47018  fourierdlem42  47432  fourierdlem48  47437  fourierdlem50  47439  fourierdlem51  47440  fourierdlem54  47443  fourierdlem86  47475  ovnval2  47828  ovnsubaddlem1  47853  hoiqssbl  47908  vonicclem2  47967  f1cof1b  48420  f1ocof1ob2  48425  funressnbrafv2  48587  dfatdmfcoafv2  48597  2ffzoeq  48671  fundcmpsurbijinj  48765  ichreuopeq  48828  prproropf1olem4  48861  prprspr2  48873  prprsprreu  48874  prprreueq  48875  reuopreuprim  48881  nprmmul3  48884  isubgrgrim  49300  grtriprop  49312  isgrtri  49314  opgpgvtx  49426  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem4  49490  grlimedgnedg  49502  rngcsectALTV  49645  rngcinvALTV  49646  ringcsectALTV  49679  ringcinvALTV  49680  lmod1  49935  elbigo2  49995  prelrrx2bd  50157  rrx2vlinest  50184  eloprab1st2nd  50310  i0oii  50365  io1ii  50366  lubeldm2d  50403  glbeldm2d  50404  sectpropdlem  50481  invpropdlem  50483  isopropdlem  50485  uppropd  50628  functhinc  50914  fullthinc  50916