Theorem anbi1d 640

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anbi12d  641  anbi1  642  pm5.71  1041  cador  1628  drsb1  2526  eleq1w  2845  eleq1d  2847  clelab  2906  rmoeq1f  3404  rabeq  3428  rabeqbidva  3430  rabeqd  3442  rabeqf  3448  alexeqg  3610  reu2eqd  3699  sbc2or  3753  sbc5ALT  3773  rexssOLD  4012  psstr  4061  difin2  4253  r19.28z  4456  dfif6  4483  rabsneq  4601  rexreusng  4638  reurexprg  4663  rabsnifsb  4681  ssunsn2  4785  preq12bg  4811  opeq1  4831  eluni  4868  csbuni  4896  unissb  4899  iuneq12d  4979  disjxun  5098  unopab  5180  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  dftr2c  5210  axrep1  5228  axreplem  5229  zfrepclf  5241  axsepgfromrep  5244  axsepg  5247  zfauscl  5248  reusv2lem4  5358  rabxfrd  5374  opthg  5445  otthg  5453  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  opeqsng  5472  euotd  5482  elopabw  5496  pocl  5563  xpeq1  5661  elxpi  5669  vtoclr  5710  opbrop  5745  dmopab2rex  5893  resopab2  6025  rnco  6239  dflim2  6404  dffun2  6531  fun11  6595  feq2  6670  f1eq2  6756  f1eq3  6757  foeq2  6775  brprcneu  6857  brprcneuALT  6858  ssimaexg  6953  dmfco  6963  funcnvmpt  6977  fndmdif  7023  respreima  7047  isoeq5  7305  isoini  7322  isopolem  7329  f1oiso  7335  f1oiso2  7336  imaeqsexvOLD  7347  riotaeqdv  7354  oprabidw  7427  oprabid  7428  oprabv  7456  mpoeq123  7468  mpoeq123dva  7470  0mpo0  7479  eloprabga  7505  resoprab  7514  resoprab2  7515  elrnmpores  7534  ov  7540  ov3  7559  ov6g  7560  ovg  7561  imaeqexov  7634  caoftrn  7701  uniuni  7745  limuni3  7832  elxp4  7903  elxp5  7904  opabex3d  7946  opabex3rd  7947  opabex3  7948  releldmdifi  8026  opiota  8040  eloprabi  8044  mptmpoopabbrd  8062  cnvf1o  8090  frxp  8106  xporderlem  8107  poxp  8108  fnwelem  8111  poxp2  8123  xpord3pred  8132  poseq  8138  soseq  8139  suppimacnv  8154  rexsupp  8162  mpocurryd  8249  smoel2  8334  omeu  8554  oeeui  8572  omabs  8621  omopth  8632  eldifsucnn  8634  qliftel  8782  brecop  8792  eroveu  8794  erov  8796  ecopovtrn  8802  ixpsnf1o  8920  dom2lem  8973  mapsnend  9017  xpsnen  9033  xpassen  9043  pw2f1olem  9053  xpf1o  9111  unxpdom  9203  domunfican  9266  preleqALT  9572  zfinf  9594  cantnfs  9621  brttrcl  9668  ttrclselem2  9681  tcvalg  9691  r0weon  9968  fseqenlem1  9980  acni2  10002  aceq1  10073  aceq0  10074  dfac5lem4  10082  dfac2a  10086  dfac12lem2  10101  cardcf  10208  cfeq0  10213  cfsuc  10214  cff1  10215  cfss  10222  isf32lem5  10314  fin1a2lem6  10362  zfac  10417  brdom7disj  10488  brdom6disj  10489  axrepnd  10552  axunndlem1  10553  axinfnd  10564  axacndlem5  10569  axacnd  10570  zfcndrep  10572  zfcndinf  10576  zfcndac  10577  pwfseqlem4a  10619  pwfseqlem4  10620  gruina  10776  grothomex  10787  ordpipq  10900  elnpi  10946  genpass  10967  ltprord  10988  reclem2pr  11006  reclem3pr  11007  recexpr  11009  addsrmo  11031  mulsrmo  11032  addsrpr  11033  mulsrpr  11034  ltsosr  11052  mulgt0sr  11063  supsr  11070  ltresr  11098  axpre-lttrn  11124  axpre-mulgt0  11126  prime  12654  peano5uzti  12663  rexuz  12899  ltxr  13117  qbtwnre  13202  xmulneg1  13272  supxr2  13317  ixxval  13357  fzval  13514  preduz  13655  nn0opth2  14285  hashbclem  14465  hashf1lem2  14469  eqwrd  14570  pfxeq  14709  wrd2ind  14736  cshwcsh2id  14841  eqwrds3  14974  cleq1lem  14995  rtrclreclem3  15073  rtrclreclem4  15074  relexpindlem  15076  abslt  15342  absle  15343  lenegsq  15348  abs2difabs  15362  ello12  15543  elo12  15554  o1lo1  15564  rlimuni  15577  lo1resb  15591  o1resb  15593  2clim  15599  rlimcn3  15617  climcn2  15620  addcn2  15621  mulcn2  15623  o1of2  15640  sumeq1  15716  fsum2dlem  15797  modfsummod  15822  prodeq1f  15936  prodeq1  15937  fprod2dlem  16010  nndivdvds  16295  divalg2  16439  smupval  16522  gcdval  16530  gcdass  16581  lcmval  16626  lcmass  16648  rpexp  16757  pythagtriplem2  16853  pythagtrip  16870  vdwapun  17010  0ram  17056  ramub1lem2  17063  pwsle  17522  imasleval  17571  ismre  17618  ismri  17663  iscatd2  17713  dfiso2  17805  isssc  17853  funcpropd  17935  fullpropd  17955  fthres2b  17965  fthres2c  17966  setcsect  18122  cat1lem  18129  cat1  18130  prslem  18329  drsdir  18334  posi  18349  tosso  18449  odudlatb  18557  ipoval  18562  ipolt  18567  dirge  18635  gsumpropd2lem  18713  mgmhmpropd  18732  issgrpv  18755  issgrpn0  18756  ismhm0  18824  mhmpropd  18826  mndind  18862  mgmnsgrpex  18968  issubg3  19186  isga  19331  symgfixelq  19473  psgnfval  19540  psgnval  19547  dprdw  20052  subgdmdprd  20076  isomnd  20163  isrnghm  20490  issubrg  20621  resrhm2b  20652  rngcsect  20686  rngcinv  20687  ringcsect  20720  ringcinv  20721  drngpropd  20819  orngmul  20914  islmod  20931  lmodlema  20932  lmodprop2d  20991  lsslss  21028  lbspropd  21166  lbsacsbs  21226  znleval  21606  islbs4  21884  islinds3  21886  aspval2  21950  psrbag  21969  pf1ind  22418  mdetunilem4  22675  mdetunilem9  22680  istopg  22955  basis2  23011  tg2  23025  iscld  23087  isnei  23163  isneip  23165  neiptoptop  23191  neiptopnei  23192  neitr  23240  restlp  23243  iscn  23295  cnpval  23296  iscnp  23297  regsep  23394  1stcclb  23504  2ndc1stc  23511  2ndcctbss  23515  2ndcdisj  23516  llyi  23534  nllyi  23535  hausmapdom  23560  locfinnei  23583  comppfsc  23592  elkgen  23596  txbas  23627  txcls  23664  txcnpi  23668  ptpjopn  23672  txdis1cn  23695  txtube  23700  txcmplem1  23701  hausdiag  23705  tx1stc  23710  txkgen  23712  xkococn  23720  elqtop  23757  kqreglem1  23801  elmptrab  23887  isfbas  23889  elflim2  24024  elflim  24031  hauspwpwf1  24047  alexsublem  24104  ghmcnp  24175  qustgplem  24181  tsmssubm  24203  elutop  24293  ustuqtop4  24304  isucn  24337  iscfilu  24347  ispsmet  24364  ismet  24383  isxmet  24384  ismet2  24393  imasdsf1olem  24433  blres  24491  elmopn  24502  mopni  24552  neibl  24561  nrmmetd  24634  ngppropd  24697  elcncf  24951  mulc1cncf  24967  elpi1  25107  isclmp  25159  metcld2  25369  pmltpclem1  25510  itg1climres  25776  itg2val  25790  isibl  25827  itgeq1f  25833  itgeq1fOLD  25834  itgeq1  25835  cbvitgv  25839  itgresr  25841  iblcn  25861  itgfsum  25889  dvreslem  25971  dvfsumlem2  26089  deg1ldg  26152  vieta1  26376  ulm2  26448  sincosq2sgn  26564  sincosq4sgn  26566  efopn  26723  dvdsflsumcom  27252  fsumvma2  27278  logfac2  27281  dchrptlem1  27328  lgsdchrval  27418  2lgslem1a  27455  pntibndlem3  27656  pntlemi  27668  pntleme  27672  pnt3  27676  ltsval  27711  nolt02o  27759  leltstr  27825  nocvxminlem  27847  madebday  27993  ltslpss  28001  addsprop  28069  mulsproplemcbv  28208  mulsproplem1  28209  mulsprop  28223  abslts  28342  eucliddivs  28469  bdayfinbndlem2  28561  z12sge0  28576  istrkgld  28628  istrkg2ld  28629  istrkg3ld  28630  axtgsegcon  28633  axtg5seg  28634  axtgpasch  28636  axtgupdim2  28640  legov  28754  islnopp  28912  ishpg  28932  iscgra1  29004  dfcgra2  29024  dfcgrg2  29057  brprlng  29065  brcgr  29101  brbtwn2  29106  axsegconlem1  29118  axsegcon  29128  axcontlem10  29174  edgssv2  29399  uhgr2edg  29409  isfusgrf1  29521  edgnbusgreu  29568  cplgr3v  29636  vtxdun  29682  upgr2wlk  29867  upgrtrls  29900  upgristrl  29901  upgrf1istrl  29902  dfpth2  29929  2pthnloop  29931  usgr2pth  29964  isclwlke  29977  isclwlkupgr  29978  iswwlksnx  30040  wlknewwlksn  30087  2pthon3v  30143  elwwlks2on  30161  wpthswwlks2on  30164  rusgrnumwwlkl1  30171  rusgrnumwwlkb0  30174  clwwlknp  30239  clwwlkf  30249  erclwwlknsym  30272  erclwwlkntr  30273  clwwlknonwwlknonb  30308  0trl  30324  0spth  30328  0crct  30335  0cycl  30336  upgr4cycl4dv4e  30387  upgriseupth  30409  eupth2lem2  30421  3cyclfrgrrn1  30487  4cycl2vnunb  30492  frgrncvvdeqlem2  30502  frgr2wwlk1  30531  fusgr2wsp2nb  30536  numclwlk1lem1  30571  vciOLD  30764  isvclem  30780  nmoofval  30965  isph  31025  norm3lemt  31355  isch2  31426  cmbr  31787  eigre  32038  eigorth  32041  nmopub  32111  nmfnleub  32128  cvbr  32485  mdbr  32497  dmdbr  32502  chrelat2  32573  mdsymlem2  32607  rexunirn  32691  ifeqeqx  32741  iunrnmptss  32765  fdifsupp  32887  ressupprn  32892  1stpreima  32909  fpwrelmapffslem  32934  archirng  33368  isslmd  33382  slmdlema  33383  urpropd  33411  lindflbs  33565  islbs5  33566  lindfpropd  33568  opprqus0g  33678  idlsrgval  33699  ressply1mon1p  33764  ccfldextdgrr  33969  constrsslem  34038  constrconj  34042  constrlccllem  34050  constrcbvlem  34052  dya2iocuni  34580  omsfval  34591  elcarsg  34602  itgeq12dv  34623  isrrvv  34740  reprinrn  34912  reprdifc  34921  istrkg2d  34960  axtgupdim2ALTV  34962  brafs  34969  bnj956  35072  bnj1146  35086  bnj18eq1  35222  axsepg2  35436  axsepg3  35437  axsepg3ALT  35438  axsepg4  35439  axsepg5  35440  zltp1ne  35460  isacycgr  35495  kur14  35566  pconncn  35574  cnpconn  35580  txpconn  35582  cvmscbv  35608  cvmcov  35613  cvmsi  35615  cvmsval  35616  cvmopnlem  35628  cvmlift2lem10  35662  cvmlift3lem2  35670  cvmlift3lem6  35674  cvmlift3lem7  35675  cvmlift3lem9  35677  cvmlift3  35678  satf0op  35727  sat1el2xp  35729  satffunlem  35751  dmopab3rexdif  35755  mclsssvlem  35912  mclsind  35920  rexxfr3dALT  35989  eldm3  36111  opelco3  36125  dfon2lem6  36136  dfon2lem7  36137  dfon2lem8  36138  dfon2  36140  elfuns  36263  lemsuccf  36289  brofs  36355  5segofs  36356  brifs  36393  ifscgr  36394  brcolinear  36409  lineext  36426  brfs  36429  fscgr  36430  linecgr  36431  btwnconn1lem4  36440  btwnconn1lem8  36444  btwnconn1lem11  36447  btwnconn1lem12  36448  segcon2  36455  brsegle  36458  outsideofeq  36480  funray  36490  funline  36492  fvline  36494  linethru  36503  disjeq12dv  36575  prodeq12sdv  36578  itgeq12sdv  36579  cbvitgvw2  36608  cbvitgdavw  36641  cbvitgdavw2  36657  trer  36676  finminlem  36678  ivthALT  36695  filnetlem4  36741  axtco1  36833  axtco1from2  36835  ttcexg  36892  mh-infprim1bi  36906  knoppndvlem21  36970  bj-zfauscl  37409  bj-elgab  37424  bj-imdirvallem  37672  csboprabg  37824  topdifinffinlem  37841  icoreval  37847  isbasisrelowllem1  37849  isbasisrelowllem2  37850  relowlssretop  37857  pibp19  37908  curf  38097  ptrest  38118  poimirlem1  38120  poimirlem13  38132  poimirlem14  38133  poimirlem22  38141  poimirlem24  38143  poimirlem26  38145  poimirlem27  38146  heicant  38154  mblfinlem3  38158  mblfinlem4  38159  mbfresfi  38165  itg2addnclem3  38172  itg2addnc  38173  itg2gt0cn  38174  areacirclem5  38211  cover2  38214  cover2g  38215  fdc  38244  fdc1  38245  heibor1  38309  bfp  38323  rngosn3  38423  drngoi  38450  isdrngo1  38455  isriscg  38483  isfldidl2  38568  raldmqseu  38864  eldmxrncnvepres  38933  brressn  39030  islshpat  39641  lcvbr  39645  lshpsmreu  39733  ldual1dim  39790  cvrval  39893  cvrnbtwn3  39900  iscvlat2N  39948  ishlat3N  39978  hlrelat5N  40025  3dim0  40081  llnexatN  40145  islpln5  40159  islvol5  40203  pmapjat1  40477  ltrnu  40745  cdleme02N  40846  cdlemg33b  41331  cdlemg33c  41332  dvhb1dimN  41610  dibelval3  41771  dibopelval3  41772  dib1dim  41789  dibglbN  41790  diblsmopel  41795  dicval  41800  dicopelval  41801  dicelval3  41804  dicelval1sta  41811  dihopelvalcpre  41872  dih1dimatlem  41953  dihpN  41960  dihjatcclem4  42045  lpolsetN  42106  mapdpglem3  42299  hdmapglem7a  42551  sticksstones23  42786  exfinfldd  42820  fimgmcyclem  43151  fimgmcyc  43152  fsuppind  43172  fsuppssindlem2  43174  prjspeclsp  43194  mrefg2  43288  mzpclval  43306  eldiophb  43338  eldioph2lem1  43341  eldioph3  43347  lzenom  43351  diophin  43353  eldiophss  43355  diophrex  43356  eq0rabdioph  43357  pellexlem3  43408  elpell1qr  43424  elpell14qr  43426  elpell1234qr  43428  jm2.27  43585  rmydioph  43591  expdiophlem1  43598  expdioph  43600  pw2f1ocnv  43614  hbtlem1  43700  hbtlem7  43702  dgraalem  43722  dgraaub  43725  dflim7  43850  omabs2  43909  tfsconcatfv2  43917  tfsconcat0i  43922  nadd1suc  43969  ifpbi2  44043  inintabd  44155  cnvcnvintabd  44176  cnvintabd  44179  clcnvlem  44199  iunrelexpmin1  44284  uneqsn  44601  k0004lem2  44724  mnuprdlem1  44848  mnuprdlem2  44849  binomcxplemnotnn0  44932  2sbc6g  44991  2sbc5g  44992  iotasbc  44995  dropab1  45022  dropab2  45023  relpeq5  45524  modelaxreplem3  45556  omssaxinf2  45564  brpermmodel  45579  permaxinf2lem  45588  cbvmpo1  45676  r19.28zf  45737  disjinfi  45770  dmrelrnrel  45802  mullimc  46192  mullimcf  46199  limsuppnfd  46276  limsuppnf  46285  limsupre2  46299  limsupre2mpt  46304  limsupre3  46307  limsupre3mpt  46308  limsupre3uzlem  46309  fourierdlem42  46723  fourierdlem48  46728  fourierdlem50  46730  fourierdlem51  46731  fourierdlem54  46734  fourierdlem86  46766  ovnval2  47119  ovnsubaddlem1  47144  hoiqssbl  47199  vonicclem2  47258  f1cof1b  47671  f1ocof1ob2  47676  funressnbrafv2  47838  dfatdmfcoafv2  47848  2ffzoeq  47922  fundcmpsurbijinj  48016  ichreuopeq  48079  prproropf1olem4  48112  prprspr2  48124  prprsprreu  48125  prprreueq  48126  reuopreuprim  48132  nprmmul3  48135  isubgrgrim  48551  grtriprop  48563  isgrtri  48565  opgpgvtx  48677  pgnbgreunbgrlem1  48735  pgnbgreunbgrlem4  48741  grlimedgnedg  48753  rngcsectALTV  48897  rngcinvALTV  48898  ringcsectALTV  48931  ringcinvALTV  48932  lmod1  49114  elbigo2  49174  rrx2vlinest  49363  eloprab1st2nd  49489  i0oii  49541  io1ii  49542  lubeldm2d  49579  glbeldm2d  49580  sectpropdlem  49657  invpropdlem  49659  isopropdlem  49661  uppropd  49802  functhinc  50069  fullthinc  50071