Theorem anbi1d 630

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 205   ∧ 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 206  df-an 397

This theorem is referenced by:  anbi12d  631  anbi1  632  pm5.71  1026  cador  1609  drsb1  2493  eleq1w  2815  eleq1d  2817  clelab  2878  rexeqf  3327  rmoeq1  3389  reueq1  3390  rmoeq1f  3393  reueq1f  3394  rabeq  3419  rabeqd  3434  rabeqf  3439  rabeqiOLD  3443  cgsex4g  3491  vtocl2gaf  3537  vtocl4ga  3542  alexeqg  3604  elrabiOLD  3643  reu2eqd  3697  sbc2or  3751  sbc5ALT  3771  rexss  4020  psstr  4069  difin2  4256  r19.28z  4460  dfif6  4494  rexreusng  4645  reurexprg  4670  rabsnifsb  4688  ssunsn2  4792  preq12bg  4816  opeq1  4835  eluni  4873  csbuni  4902  unissb  4905  disjxun  5108  unopab  5192  mpteq12da  5195  mpteq12f  5198  mpteq12dva  5199  dftr2c  5230  axrep1  5248  axreplem  5249  zfrepclf  5256  axsepgfromrep  5259  axsepg  5262  zfauscl  5263  reusv2lem4  5361  rabxfrd  5377  opthg  5439  otthg  5447  copsexgw  5452  copsexg  5453  opeqsng  5465  euotd  5475  elopabw  5488  pocl  5557  poclOLD  5558  xpeq1  5652  elxpi  5660  vtoclr  5700  opbrop  5734  dmopab2rex  5878  resopab2  5995  dflim2  6379  dffun2  6511  fun11  6580  feq2  6655  f1eq2  6739  f1eq3  6740  foeq2  6758  brprcneu  6837  brprcneuALT  6838  ssimaexg  6932  dmfco  6942  fndmdif  6997  respreima  7021  isoeq5  7271  isoini  7288  isopolem  7295  f1oiso  7301  f1oiso2  7302  imaeqsexv  7313  riotaeqdv  7319  oprabidw  7393  oprabid  7394  oprabv  7422  mpoeq123  7434  mpoeq123dva  7436  0mpo0  7445  eloprabga  7469  eloprabgaOLD  7470  resoprab  7479  resoprab2  7480  elrnmpores  7498  ov  7504  ov3  7522  ov6g  7523  ovg  7524  imaeqexov  7597  caoftrn  7660  uniuni  7701  limuni3  7793  elxp4  7864  elxp5  7865  opabex3d  7903  opabex3rd  7904  opabex3  7905  releldmdifi  7982  opiota  7996  eloprabi  8000  mptmpoopabbrd  8018  mptmpoopabbrdOLD  8020  cnvf1o  8048  frxp  8063  xporderlem  8064  poxp  8065  fnwelem  8068  poxp2  8080  xpord3pred  8089  poseq  8095  soseq  8096  suppimacnv  8110  rexsupp  8118  mpocurryd  8205  smoel2  8314  omeu  8537  oeeui  8554  omabs  8602  omopth  8613  eldifsucnn  8615  qliftel  8746  brecop  8756  eroveu  8758  erov  8760  ecopovtrn  8766  ixpsnf1o  8883  dom2lem  8939  mapsnend  8987  xpsnen  9006  xpassen  9017  pw2f1olem  9027  xpf1o  9090  unxpdom  9204  domunfican  9271  preleqALT  9562  zfinf  9584  cantnfs  9611  brttrcl  9658  ttrclselem2  9671  tcvalg  9683  r0weon  9957  fseqenlem1  9969  acni2  9991  aceq1  10062  aceq0  10063  dfac2a  10074  dfac12lem2  10089  cardcf  10197  cfeq0  10201  cfsuc  10202  cff1  10203  cfss  10210  isf32lem5  10302  fin1a2lem6  10350  zfac  10405  brdom7disj  10476  brdom6disj  10477  axrepnd  10539  axunndlem1  10540  axinfnd  10551  axacndlem5  10556  axacnd  10557  zfcndrep  10559  zfcndinf  10563  zfcndac  10564  pwfseqlem4a  10606  pwfseqlem4  10607  gruina  10763  grothomex  10774  ordpipq  10887  elnpi  10933  genpass  10954  ltprord  10975  reclem2pr  10993  reclem3pr  10994  recexpr  10996  addsrmo  11018  mulsrmo  11019  addsrpr  11020  mulsrpr  11021  ltsosr  11039  mulgt0sr  11050  supsr  11057  ltresr  11085  axpre-lttrn  11111  axpre-mulgt0  11113  prime  12593  peano5uzti  12602  rexuz  12832  ltxr  13045  qbtwnre  13128  xmulneg1  13198  supxr2  13243  ixxval  13282  fzval  13436  preduz  13573  nn0opth2  14182  hashbclem  14361  hashf1lem2  14367  eqwrd  14457  pfxeq  14596  wrd2ind  14623  cshwcsh2id  14729  eqwrds3  14862  cleq1lem  14879  rtrclreclem3  14957  rtrclreclem4  14958  relexpindlem  14960  abslt  15211  absle  15212  lenegsq  15217  abs2difabs  15231  ello12  15410  elo12  15421  o1lo1  15431  rlimuni  15444  lo1resb  15458  o1resb  15460  2clim  15466  rlimcn3  15484  climcn2  15487  addcn2  15488  mulcn2  15490  o1of2  15507  sumeq1  15585  fsum2dlem  15666  modfsummod  15690  prodeq1f  15802  fprod2dlem  15874  nndivdvds  16156  divalg2  16298  smupval  16379  gcdval  16387  gcdass  16439  lcmval  16479  lcmass  16501  rpexp  16609  pythagtriplem2  16700  pythagtrip  16717  vdwapun  16857  0ram  16903  ramub1lem2  16910  pwsle  17388  imasleval  17437  ismre  17484  ismri  17525  iscatd2  17575  dfiso2  17669  isssc  17717  funcpropd  17801  fullpropd  17821  fthres2b  17831  fthres2c  17832  setcsect  17989  cat1lem  17996  cat1  17997  prslem  18201  drsdir  18205  posi  18220  tosso  18322  odudlatb  18428  ipoval  18433  ipolt  18438  dirge  18506  gsumpropd2lem  18548  issgrpv  18562  issgrpn0  18563  mhmpropd  18622  mndind  18652  mgmnsgrpex  18755  issubg3  18960  isga  19085  symgfixelq  19229  psgnfval  19296  psgnval  19303  dprdw  19803  subgdmdprd  19827  drngpropd  20259  issubrg  20270  resrhm2b  20301  islmod  20382  lmodlema  20383  lmodprop2d  20441  lsslss  20479  lbspropd  20617  lbsacsbs  20676  znleval  20998  islbs4  21275  islinds3  21277  aspval2  21338  psrbag  21356  pf1ind  21758  mdetunilem4  22001  mdetunilem9  22006  istopg  22281  basis2  22338  tg2  22352  iscld  22415  isnei  22491  isneip  22493  neiptoptop  22519  neiptopnei  22520  neitr  22568  restlp  22571  iscn  22623  cnpval  22624  iscnp  22625  regsep  22722  1stcclb  22832  2ndc1stc  22839  2ndcctbss  22843  2ndcdisj  22844  llyi  22862  nllyi  22863  hausmapdom  22888  locfinnei  22911  comppfsc  22920  elkgen  22924  txbas  22955  txcls  22992  txcnpi  22996  ptpjopn  23000  txdis1cn  23023  txtube  23028  txcmplem1  23029  hausdiag  23033  tx1stc  23038  txkgen  23040  xkococn  23048  elqtop  23085  kqreglem1  23129  elmptrab  23215  isfbas  23217  elflim2  23352  elflim  23359  hauspwpwf1  23375  alexsublem  23432  ghmcnp  23503  qustgplem  23509  tsmssubm  23531  elutop  23622  ustuqtop4  23633  isucn  23667  iscfilu  23677  ispsmet  23694  ismet  23713  isxmet  23714  ismet2  23723  imasdsf1olem  23763  blres  23821  elmopn  23832  mopni  23885  neibl  23894  nrmmetd  23967  ngppropd  24030  elcncf  24289  mulc1cncf  24305  elpi1  24445  isclmp  24497  metcld2  24708  pmltpclem1  24849  itg1climres  25116  itg2val  25130  isibl  25167  itgeq1f  25173  itgresr  25180  iblcn  25200  itgfsum  25228  dvreslem  25310  dvfsumlem2  25428  deg1ldg  25494  vieta1  25709  ulm2  25781  sincosq2sgn  25893  sincosq4sgn  25895  efopn  26050  dvdsflsumcom  26574  fsumvma2  26599  logfac2  26602  dchrptlem1  26649  lgsdchrval  26739  2lgslem1a  26776  pntibndlem3  26977  pntlemi  26989  pntleme  26993  pnt3  26997  sltval  27032  nolt02o  27080  slelttr  27142  nocvxminlem  27160  madebday  27272  sltlpss  27279  addsprop  27331  mulsproplem1  27422  istrkgld  27464  istrkg2ld  27465  istrkg3ld  27466  axtgsegcon  27469  axtg5seg  27470  axtgpasch  27472  axtgupdim2  27476  legov  27590  islnopp  27744  ishpg  27764  iscgra1  27815  dfcgra2  27835  dfcgrg2  27868  brcgr  27912  brbtwn2  27917  axsegconlem1  27929  axsegcon  27939  axcontlem10  27985  edgssv2  28209  uhgr2edg  28219  isfusgrf1  28331  edgnbusgreu  28378  cplgr3v  28446  vtxdun  28492  upgr2wlk  28679  upgrtrls  28712  upgristrl  28713  upgrf1istrl  28714  2pthnloop  28742  usgr2pth  28775  isclwlke  28788  isclwlkupgr  28789  iswwlksnx  28848  wlknewwlksn  28895  2pthon3v  28951  elwwlks2on  28967  wpthswwlks2on  28969  rusgrnumwwlkl1  28976  rusgrnumwwlkb0  28979  clwwlknp  29044  clwwlkf  29054  erclwwlknsym  29077  erclwwlkntr  29078  clwwlknonwwlknonb  29113  0trl  29129  0spth  29133  0crct  29140  0cycl  29141  upgr4cycl4dv4e  29192  upgriseupth  29214  eupth2lem2  29226  3cyclfrgrrn1  29292  4cycl2vnunb  29297  frgrncvvdeqlem2  29307  frgr2wwlk1  29336  fusgr2wsp2nb  29341  numclwlk1lem1  29376  vciOLD  29566  isvclem  29582  nmoofval  29767  isph  29827  norm3lemt  30157  isch2  30228  cmbr  30589  eigre  30840  eigorth  30843  nmopub  30913  nmfnleub  30930  cvbr  31287  mdbr  31299  dmdbr  31304  chrelat2  31375  mdsymlem2  31409  rexunirn  31484  ifeqeqx  31528  iunrnmptss  31551  funcnvmpt  31650  ressupprn  31672  1stpreima  31688  fpwrelmapffslem  31717  isomnd  31979  archirng  32094  isslmd  32107  slmdlema  32108  orngmul  32169  lindflbs  32239  islbs5  32240  lindfpropd  32242  idlsrgval  32321  ressply1mon1p  32356  ccfldextdgrr  32443  dya2iocuni  32972  omsfval  32983  elcarsg  32994  itgeq12dv  33015  isrrvv  33132  reprinrn  33320  reprdifc  33329  istrkg2d  33368  axtgupdim2ALTV  33370  brafs  33374  bnj956  33477  bnj1146  33492  bnj18eq1  33628  zltp1ne  33789  isacycgr  33826  kur14  33897  pconncn  33905  cnpconn  33911  txpconn  33913  cvmscbv  33939  cvmcov  33944  cvmsi  33946  cvmsval  33947  cvmopnlem  33959  cvmlift2lem10  33993  cvmlift3lem2  34001  cvmlift3lem6  34005  cvmlift3lem7  34006  cvmlift3lem9  34008  cvmlift3  34009  satf0op  34058  sat1el2xp  34060  satffunlem  34082  dmopab3rexdif  34086  mclsssvlem  34243  mclsind  34251  eldm3  34420  opelco3  34435  dfon2lem6  34449  dfon2lem7  34450  dfon2lem8  34451  dfon2  34453  elfuns  34576  brsuccf  34602  brofs  34666  5segofs  34667  brifs  34704  ifscgr  34705  brcolinear  34720  lineext  34737  brfs  34740  fscgr  34741  linecgr  34742  btwnconn1lem4  34751  btwnconn1lem8  34755  btwnconn1lem11  34758  btwnconn1lem12  34759  segcon2  34766  brsegle  34769  outsideofeq  34791  funray  34801  funline  34803  fvline  34805  linethru  34814  trer  34864  finminlem  34866  ivthALT  34883  filnetlem4  34929  knoppndvlem21  35071  bj-zfauscl  35467  bj-elgab  35482  bj-imdirvallem  35724  csboprabg  35874  topdifinffinlem  35891  icoreval  35897  isbasisrelowllem1  35899  isbasisrelowllem2  35900  relowlssretop  35907  pibp19  35958  wl-ax11-lem8  36117  curf  36129  ptrest  36150  poimirlem1  36152  poimirlem13  36164  poimirlem14  36165  poimirlem22  36173  poimirlem24  36175  poimirlem26  36177  poimirlem27  36178  heicant  36186  mblfinlem3  36190  mblfinlem4  36191  mbfresfi  36197  itg2addnclem3  36204  itg2addnc  36205  itg2gt0cn  36206  areacirclem5  36243  cover2  36246  cover2g  36247  fdc  36277  fdc1  36278  heibor1  36342  bfp  36356  rngosn3  36456  drngoi  36483  isdrngo1  36488  isriscg  36516  isfldidl2  36601  brressn  36976  islshpat  37552  lcvbr  37556  lshpsmreu  37644  ldual1dim  37701  cvrval  37804  cvrnbtwn3  37811  iscvlat2N  37859  ishlat3N  37889  hlrelat5N  37937  3dim0  37993  llnexatN  38057  islpln5  38071  islvol5  38115  pmapjat1  38389  ltrnu  38657  cdleme02N  38758  cdlemg33b  39243  cdlemg33c  39244  dvhb1dimN  39522  dibelval3  39683  dibopelval3  39684  dib1dim  39701  dibglbN  39702  diblsmopel  39707  dicval  39712  dicopelval  39713  dicelval3  39716  dicelval1sta  39723  dihopelvalcpre  39784  dih1dimatlem  39865  dihpN  39872  dihjatcclem4  39957  lpolsetN  40018  mapdpglem3  40211  hdmapglem7a  40463  fsuppind  40823  fsuppssindlem2  40825  prjspeclsp  41008  mrefg2  41088  mzpclval  41106  eldiophb  41138  eldioph2lem1  41141  eldioph3  41147  lzenom  41151  diophin  41153  eldiophss  41155  diophrex  41156  eq0rabdioph  41157  pellexlem3  41212  elpell1qr  41228  elpell14qr  41230  elpell1234qr  41232  jm2.27  41390  rmydioph  41396  expdiophlem1  41403  expdioph  41405  pw2f1ocnv  41419  hbtlem1  41508  hbtlem7  41510  dgraalem  41530  dgraaub  41533  dflim7  41666  omabs2  41725  tfsconcatfv2  41733  tfsconcat0i  41738  nadd1suc  41785  ifpbi2  41861  inintabd  41973  cnvcnvintabd  41994  cnvintabd  41997  clcnvlem  42017  iunrelexpmin1  42102  uneqsn  42419  k0004lem2  42542  mnuprdlem1  42674  mnuprdlem2  42675  binomcxplemnotnn0  42758  2sbc6g  42817  2sbc5g  42818  iotasbc  42821  dropab1  42849  dropab2  42850  cbvmpo1  43430  r19.28zf  43496  disjinfi  43534  dmrelrnrel  43568  mullimc  43977  mullimcf  43984  limsuppnfd  44063  limsuppnf  44072  limsupre2  44086  limsupre2mpt  44091  limsupre3  44094  limsupre3mpt  44095  limsupre3uzlem  44096  fourierdlem42  44510  fourierdlem48  44515  fourierdlem50  44517  fourierdlem51  44518  fourierdlem54  44521  fourierdlem86  44553  ovnval2  44906  ovnsubaddlem1  44931  hoiqssbl  44986  vonicclem2  45045  f1cof1b  45429  f1ocof1ob2  45434  funressnbrafv2  45596  dfatdmfcoafv2  45606  2ffzoeq  45680  fundcmpsurbijinj  45722  ichreuopeq  45785  prproropf1olem4  45818  prprspr2  45830  prprsprreu  45831  prprreueq  45832  reuopreuprim  45838  mgmhmpropd  46199  ismhm0  46219  isrnghm  46310  rngcsect  46398  rngcinv  46399  rngcsectALTV  46410  rngcinvALTV  46411  ringcsect  46449  ringcinv  46450  ringcsectALTV  46473  ringcinvALTV  46474  lmod1  46693  elbigo2  46758  rrx2vlinest  46947  i0oii  47072  io1ii  47073  lubeldm2d  47111  glbeldm2d  47112  functhinc  47185  fullthinc  47186