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  3331  rmoeq1OLD  3389  reueq1OLD  3390  rmoeq1f  3395  rabeq  3420  rabeqbidva  3422  rabeqd  3434  rabeqf  3440  cgsex4gOLD  3495  vtocl2gafOLD  3546  vtocl4gaOLD  3553  alexeqg  3617  reu2eqd  3707  sbc2or  3762  sbc5ALT  3782  rexssOLD  4024  psstr  4070  difin2  4264  r19.28z  4461  dfif6  4491  rabsneq  4608  rexreusng  4643  reurexprg  4668  rabsnifsb  4686  ssunsn2  4791  preq12bg  4817  opeq1  4837  eluni  4874  csbuni  4900  unissb  4903  iuneq12d  4985  disjxun  5105  unopab  5187  mpteq12da  5190  mpteq12f  5192  mpteq12dva  5193  dftr2c  5217  axrep1  5235  axreplem  5236  zfrepclf  5246  axsepgfromrep  5249  axsepg  5252  zfauscl  5253  reusv2lem4  5356  rabxfrd  5372  opthg  5437  otthg  5445  copsexgw  5450  copsexg  5451  opeqsng  5463  euotd  5473  elopabw  5486  pocl  5554  xpeq1  5652  elxpi  5660  vtoclr  5701  opbrop  5736  dmopab2rex  5881  resopab2  6007  dflim2  6390  dffun2  6521  fun11  6590  feq2  6667  f1eq2  6752  f1eq3  6753  foeq2  6769  brprcneu  6848  brprcneuALT  6849  ssimaexg  6947  dmfco  6957  fndmdif  7014  respreima  7038  isoeq5  7296  isoini  7313  isopolem  7320  f1oiso  7326  f1oiso2  7327  imaeqsexvOLD  7338  riotaeqdv  7345  oprabidw  7418  oprabid  7419  oprabv  7449  mpoeq123  7461  mpoeq123dva  7463  0mpo0  7472  eloprabga  7498  resoprab  7507  resoprab2  7508  elrnmpores  7527  ov  7533  ov3  7552  ov6g  7553  ovg  7554  imaeqexov  7627  caoftrn  7694  uniuni  7738  limuni3  7828  elxp4  7898  elxp5  7899  opabex3d  7944  opabex3rd  7945  opabex3  7946  releldmdifi  8024  opiota  8038  eloprabi  8042  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabbrdOLDOLD  8062  cnvf1o  8090  frxp  8105  xporderlem  8106  poxp  8107  fnwelem  8110  poxp2  8122  xpord3pred  8131  poseq  8137  soseq  8138  suppimacnv  8153  rexsupp  8161  mpocurryd  8248  smoel2  8332  omeu  8549  oeeui  8566  omabs  8615  omopth  8626  eldifsucnn  8628  qliftel  8773  brecop  8783  eroveu  8785  erov  8787  ecopovtrn  8793  ixpsnf1o  8911  dom2lem  8963  mapsnend  9007  xpsnen  9025  xpassen  9035  pw2f1olem  9045  xpf1o  9103  unxpdom  9200  domunfican  9272  preleqALT  9570  zfinf  9592  cantnfs  9619  brttrcl  9666  ttrclselem2  9679  tcvalg  9691  r0weon  9965  fseqenlem1  9977  acni2  9999  aceq1  10070  aceq0  10071  dfac5lem4  10079  dfac2a  10083  dfac12lem2  10098  cardcf  10205  cfeq0  10209  cfsuc  10210  cff1  10211  cfss  10218  isf32lem5  10310  fin1a2lem6  10358  zfac  10413  brdom7disj  10484  brdom6disj  10485  axrepnd  10547  axunndlem1  10548  axinfnd  10559  axacndlem5  10564  axacnd  10565  zfcndrep  10567  zfcndinf  10571  zfcndac  10572  pwfseqlem4a  10614  pwfseqlem4  10615  gruina  10771  grothomex  10782  ordpipq  10895  elnpi  10941  genpass  10962  ltprord  10983  reclem2pr  11001  reclem3pr  11002  recexpr  11004  addsrmo  11026  mulsrmo  11027  addsrpr  11028  mulsrpr  11029  ltsosr  11047  mulgt0sr  11058  supsr  11065  ltresr  11093  axpre-lttrn  11119  axpre-mulgt0  11121  prime  12615  peano5uzti  12624  rexuz  12857  ltxr  13075  qbtwnre  13159  xmulneg1  13229  supxr2  13274  ixxval  13314  fzval  13470  preduz  13611  nn0opth2  14237  hashbclem  14417  hashf1lem2  14421  eqwrd  14522  pfxeq  14661  wrd2ind  14688  cshwcsh2id  14794  eqwrds3  14927  cleq1lem  14948  rtrclreclem3  15026  rtrclreclem4  15027  relexpindlem  15029  abslt  15281  absle  15282  lenegsq  15287  abs2difabs  15301  ello12  15482  elo12  15493  o1lo1  15503  rlimuni  15516  lo1resb  15530  o1resb  15532  2clim  15538  rlimcn3  15556  climcn2  15559  addcn2  15560  mulcn2  15562  o1of2  15579  sumeq1  15655  fsum2dlem  15736  modfsummod  15760  prodeq1f  15872  prodeq1  15873  fprod2dlem  15946  nndivdvds  16231  divalg2  16375  smupval  16458  gcdval  16466  gcdass  16517  lcmval  16562  lcmass  16584  rpexp  16692  pythagtriplem2  16788  pythagtrip  16805  vdwapun  16945  0ram  16991  ramub1lem2  16998  pwsle  17455  imasleval  17504  ismre  17551  ismri  17592  iscatd2  17642  dfiso2  17734  isssc  17782  funcpropd  17864  fullpropd  17884  fthres2b  17894  fthres2c  17895  setcsect  18051  cat1lem  18058  cat1  18059  prslem  18258  drsdir  18263  posi  18278  tosso  18378  odudlatb  18484  ipoval  18489  ipolt  18494  dirge  18562  gsumpropd2lem  18606  mgmhmpropd  18625  issgrpv  18648  issgrpn0  18649  ismhm0  18717  mhmpropd  18719  mndind  18755  mgmnsgrpex  18858  issubg3  19076  isga  19223  symgfixelq  19363  psgnfval  19430  psgnval  19437  dprdw  19942  subgdmdprd  19966  isrnghm  20350  issubrg  20480  resrhm2b  20511  rngcsect  20545  rngcinv  20546  ringcsect  20579  ringcinv  20580  drngpropd  20678  islmod  20770  lmodlema  20771  lmodprop2d  20830  lsslss  20867  lbspropd  21006  lbsacsbs  21066  znleval  21464  islbs4  21741  islinds3  21743  aspval2  21807  psrbag  21826  pf1ind  22242  mdetunilem4  22502  mdetunilem9  22507  istopg  22782  basis2  22838  tg2  22852  iscld  22914  isnei  22990  isneip  22992  neiptoptop  23018  neiptopnei  23019  neitr  23067  restlp  23070  iscn  23122  cnpval  23123  iscnp  23124  regsep  23221  1stcclb  23331  2ndc1stc  23338  2ndcctbss  23342  2ndcdisj  23343  llyi  23361  nllyi  23362  hausmapdom  23387  locfinnei  23410  comppfsc  23419  elkgen  23423  txbas  23454  txcls  23491  txcnpi  23495  ptpjopn  23499  txdis1cn  23522  txtube  23527  txcmplem1  23528  hausdiag  23532  tx1stc  23537  txkgen  23539  xkococn  23547  elqtop  23584  kqreglem1  23628  elmptrab  23714  isfbas  23716  elflim2  23851  elflim  23858  hauspwpwf1  23874  alexsublem  23931  ghmcnp  24002  qustgplem  24008  tsmssubm  24030  elutop  24121  ustuqtop4  24132  isucn  24165  iscfilu  24175  ispsmet  24192  ismet  24211  isxmet  24212  ismet2  24221  imasdsf1olem  24261  blres  24319  elmopn  24330  mopni  24380  neibl  24389  nrmmetd  24462  ngppropd  24525  elcncf  24782  mulc1cncf  24798  elpi1  24945  isclmp  24997  metcld2  25207  pmltpclem1  25349  itg1climres  25615  itg2val  25629  isibl  25666  itgeq1f  25672  itgeq1fOLD  25673  itgeq1  25674  cbvitgv  25678  itgresr  25680  iblcn  25700  itgfsum  25728  dvreslem  25810  dvfsumlem2  25933  dvfsumlem2OLD  25934  deg1ldg  25997  vieta1  26220  ulm2  26294  sincosq2sgn  26408  sincosq4sgn  26410  efopn  26567  dvdsflsumcom  27098  fsumvma2  27125  logfac2  27128  dchrptlem1  27175  lgsdchrval  27265  2lgslem1a  27302  pntibndlem3  27503  pntlemi  27515  pntleme  27519  pnt3  27523  sltval  27559  nolt02o  27607  slelttr  27669  nocvxminlem  27689  madebday  27811  sltlpss  27819  addsprop  27883  mulsproplemcbv  28018  mulsproplem1  28019  mulsprop  28033  absslt  28151  eucliddivs  28265  zs12ge0  28342  istrkgld  28386  istrkg2ld  28387  istrkg3ld  28388  axtgsegcon  28391  axtg5seg  28392  axtgpasch  28394  axtgupdim2  28398  legov  28512  islnopp  28666  ishpg  28686  iscgra1  28737  dfcgra2  28757  dfcgrg2  28790  brcgr  28827  brbtwn2  28832  axsegconlem1  28844  axsegcon  28854  axcontlem10  28900  edgssv2  29125  uhgr2edg  29135  isfusgrf1  29247  edgnbusgreu  29294  cplgr3v  29362  vtxdun  29409  upgr2wlk  29596  upgrtrls  29629  upgristrl  29630  upgrf1istrl  29631  dfpth2  29659  2pthnloop  29661  usgr2pth  29694  isclwlke  29707  isclwlkupgr  29708  iswwlksnx  29770  wlknewwlksn  29817  2pthon3v  29873  elwwlks2on  29889  wpthswwlks2on  29891  rusgrnumwwlkl1  29898  rusgrnumwwlkb0  29901  clwwlknp  29966  clwwlkf  29976  erclwwlknsym  29999  erclwwlkntr  30000  clwwlknonwwlknonb  30035  0trl  30051  0spth  30055  0crct  30062  0cycl  30063  upgr4cycl4dv4e  30114  upgriseupth  30136  eupth2lem2  30148  3cyclfrgrrn1  30214  4cycl2vnunb  30219  frgrncvvdeqlem2  30229  frgr2wwlk1  30258  fusgr2wsp2nb  30263  numclwlk1lem1  30298  vciOLD  30490  isvclem  30506  nmoofval  30691  isph  30751  norm3lemt  31081  isch2  31152  cmbr  31513  eigre  31764  eigorth  31767  nmopub  31837  nmfnleub  31854  cvbr  32211  mdbr  32223  dmdbr  32228  chrelat2  32299  mdsymlem2  32333  rexunirn  32421  ifeqeqx  32471  iunrnmptss  32494  funcnvmpt  32591  fdifsupp  32608  ressupprn  32613  1stpreima  32630  fpwrelmapffslem  32655  isomnd  33015  archirng  33142  isslmd  33155  slmdlema  33156  urpropd  33183  orngmul  33281  lindflbs  33350  islbs5  33351  lindfpropd  33353  opprqus0g  33461  idlsrgval  33474  ressply1mon1p  33537  ccfldextdgrr  33667  constrsslem  33731  constrconj  33735  constrlccllem  33743  constrcbvlem  33745  dya2iocuni  34274  omsfval  34285  elcarsg  34296  itgeq12dv  34317  isrrvv  34434  reprinrn  34609  reprdifc  34618  istrkg2d  34657  axtgupdim2ALTV  34659  brafs  34663  bnj956  34766  bnj1146  34781  bnj18eq1  34917  axsepg2  35072  axsepg2ALT  35073  zltp1ne  35097  isacycgr  35132  kur14  35203  pconncn  35211  cnpconn  35217  txpconn  35219  cvmscbv  35245  cvmcov  35250  cvmsi  35252  cvmsval  35253  cvmopnlem  35265  cvmlift2lem10  35299  cvmlift3lem2  35307  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  cvmlift3  35315  satf0op  35364  sat1el2xp  35366  satffunlem  35388  dmopab3rexdif  35392  mclsssvlem  35549  mclsind  35557  rexxfr3dALT  35626  eldm3  35748  opelco3  35762  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  dfon2  35780  elfuns  35903  brsuccf  35929  brofs  35993  5segofs  35994  brifs  36031  ifscgr  36032  brcolinear  36047  lineext  36064  brfs  36067  fscgr  36068  linecgr  36069  btwnconn1lem4  36078  btwnconn1lem8  36082  btwnconn1lem11  36085  btwnconn1lem12  36086  segcon2  36093  brsegle  36096  outsideofeq  36118  funray  36128  funline  36130  fvline  36132  linethru  36141  disjeq12dv  36203  prodeq12sdv  36206  itgeq12sdv  36207  cbvitgvw2  36236  cbvitgdavw  36269  cbvitgdavw2  36285  trer  36304  finminlem  36306  ivthALT  36323  filnetlem4  36369  knoppndvlem21  36520  bj-zfauscl  36912  bj-elgab  36927  bj-imdirvallem  37168  csboprabg  37318  topdifinffinlem  37335  icoreval  37341  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  pibp19  37402  wl-ax11-lem8  37580  curf  37592  ptrest  37613  poimirlem1  37615  poimirlem13  37627  poimirlem14  37628  poimirlem22  37636  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  heicant  37649  mblfinlem3  37653  mblfinlem4  37654  mbfresfi  37660  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  areacirclem5  37706  cover2  37709  cover2g  37710  fdc  37739  fdc1  37740  heibor1  37804  bfp  37818  rngosn3  37918  drngoi  37945  isdrngo1  37950  isriscg  37978  isfldidl2  38063  eldmxrncnvepres  38396  brressn  38432  islshpat  39010  lcvbr  39014  lshpsmreu  39102  ldual1dim  39159  cvrval  39262  cvrnbtwn3  39269  iscvlat2N  39317  ishlat3N  39347  hlrelat5N  39395  3dim0  39451  llnexatN  39515  islpln5  39529  islvol5  39573  pmapjat1  39847  ltrnu  40115  cdleme02N  40216  cdlemg33b  40701  cdlemg33c  40702  dvhb1dimN  40980  dibelval3  41141  dibopelval3  41142  dib1dim  41159  dibglbN  41160  diblsmopel  41165  dicval  41170  dicopelval  41171  dicelval3  41174  dicelval1sta  41181  dihopelvalcpre  41242  dih1dimatlem  41323  dihpN  41330  dihjatcclem4  41415  lpolsetN  41476  mapdpglem3  41669  hdmapglem7a  41921  sticksstones23  42157  exfinfldd  42191  fimgmcyclem  42521  fimgmcyc  42522  fsuppind  42578  fsuppssindlem2  42580  prjspeclsp  42600  mrefg2  42695  mzpclval  42713  eldiophb  42745  eldioph2lem1  42748  eldioph3  42754  lzenom  42758  diophin  42760  eldiophss  42762  diophrex  42763  eq0rabdioph  42764  pellexlem3  42819  elpell1qr  42835  elpell14qr  42837  elpell1234qr  42839  jm2.27  42997  rmydioph  43003  expdiophlem1  43010  expdioph  43012  pw2f1ocnv  43026  hbtlem1  43112  hbtlem7  43114  dgraalem  43134  dgraaub  43137  dflim7  43262  omabs2  43321  tfsconcatfv2  43329  tfsconcat0i  43334  nadd1suc  43381  ifpbi2  43456  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  clcnvlem  43612  iunrelexpmin1  43697  uneqsn  44014  k0004lem2  44137  mnuprdlem1  44261  mnuprdlem2  44262  binomcxplemnotnn0  44345  2sbc6g  44404  2sbc5g  44405  iotasbc  44408  dropab1  44436  dropab2  44437  relpeq5  44938  modelaxreplem3  44970  omssaxinf2  44978  brpermmodel  44993  permaxinf2lem  45002  cbvmpo1  45092  r19.28zf  45153  disjinfi  45186  dmrelrnrel  45220  mullimc  45614  mullimcf  45621  limsuppnfd  45700  limsuppnf  45709  limsupre2  45723  limsupre2mpt  45728  limsupre3  45731  limsupre3mpt  45732  limsupre3uzlem  45733  fourierdlem42  46147  fourierdlem48  46152  fourierdlem50  46154  fourierdlem51  46155  fourierdlem54  46158  fourierdlem86  46190  ovnval2  46543  ovnsubaddlem1  46568  hoiqssbl  46623  vonicclem2  46682  f1cof1b  47078  f1ocof1ob2  47083  funressnbrafv2  47245  dfatdmfcoafv2  47255  2ffzoeq  47328  fundcmpsurbijinj  47411  ichreuopeq  47474  prproropf1olem4  47507  prprspr2  47519  prprsprreu  47520  prprreueq  47521  reuopreuprim  47527  isubgrgrim  47929  grtriprop  47940  isgrtri  47942  opgpgvtx  48046  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  rngcsectALTV  48263  rngcinvALTV  48264  ringcsectALTV  48297  ringcinvALTV  48298  lmod1  48481  elbigo2  48541  rrx2vlinest  48730  eloprab1st2nd  48856  i0oii  48908  io1ii  48909  lubeldm2d  48946  glbeldm2d  48947  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  uppropd  49170  functhinc  49437  fullthinc  49439