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  1025  cador  1610  drsb1  2500  eleq1w  2822  eleq1d  2824  clelab  2884  rexeqf  3334  reueq1f  3335  rmoeq1f  3336  reueq1  3345  rmoeq1  3346  rabeqf  3416  rabeqiOLD  3418  rabeq  3419  cgsex4g  3477  vtocl2gaf  3516  vtocl4ga  3521  alexeqg  3582  elrabiOLD  3620  reu2eqd  3672  sbc2or  3726  sbc5ALT  3746  rexss  3993  psstr  4040  difin2  4226  r19.28z  4429  dfif6  4463  rexreusng  4616  reurexprg  4641  rabsnifsb  4659  ssunsn2  4761  preq12bg  4785  opeq1  4805  eluni  4843  csbuni  4871  disjxun  5073  unopab  5157  mpteq12da  5160  mpteq12f  5163  mpteq12dva  5164  axrep1  5211  axreplem  5212  zfrepclf  5219  axsepgfromrep  5222  axsepg  5225  zfauscl  5226  reusv2lem4  5325  rabxfrd  5341  opthg  5393  otthg  5401  copsexgw  5405  copsexg  5406  opeqsng  5418  euotd  5428  elopabw  5440  pocl  5511  poclOLD  5512  xpeq1  5604  elxpi  5612  vtoclr  5651  opbrop  5685  dmopab2rex  5829  resopab2  5947  dflim2  6326  fun11  6515  feq2  6591  f1eq2  6675  f1eq3  6676  foeq2  6694  brprcneu  6773  brprcneuALT  6774  ssimaexg  6863  dmfco  6873  fndmdif  6928  respreima  6952  isoeq5  7201  isoini  7218  isopolem  7225  f1oiso  7231  f1oiso2  7232  riotaeqdv  7242  oprabidw  7315  oprabid  7316  oprabv  7344  mpoeq123  7356  mpoeq123dva  7358  0mpo0  7367  eloprabga  7391  eloprabgaOLD  7392  resoprab  7401  resoprab2  7402  elrnmpores  7420  ov  7426  ov3  7444  ov6g  7445  ovg  7446  caoftrn  7580  uniuni  7621  limuni3  7708  elxp4  7778  elxp5  7779  opabex3d  7817  opabex3rd  7818  opabex3  7819  releldmdifi  7895  opiota  7908  eloprabi  7912  mptmpoopabbrd  7930  mptmpoopabbrdOLD  7932  cnvf1o  7960  frxp  7976  xporderlem  7977  poxp  7978  fnwelem  7981  suppimacnv  7999  rexsupp  8007  mpocurryd  8094  smoel2  8203  omeu  8425  oeeui  8442  omabs  8490  omopth  8501  eldifsucnn  8503  qliftel  8598  brecop  8608  eroveu  8610  erov  8612  ecopovtrn  8618  ixpsnf1o  8735  dom2lem  8789  mapsnend  8835  xpsnen  8851  xpassen  8862  pw2f1olem  8872  xpf1o  8935  unxpdom  9039  domunfican  9096  preleqALT  9384  zfinf  9406  cantnfs  9433  brttrcl  9480  ttrclselem2  9493  tcvalg  9505  r0weon  9777  fseqenlem1  9789  acni2  9811  aceq1  9882  aceq0  9883  dfac2a  9894  dfac12lem2  9909  cardcf  10017  cfeq0  10021  cfsuc  10022  cff1  10023  cfss  10030  isf32lem5  10122  fin1a2lem6  10170  zfac  10225  brdom7disj  10296  brdom6disj  10297  axrepnd  10359  axunndlem1  10360  axinfnd  10371  axacndlem5  10376  axacnd  10377  zfcndrep  10379  zfcndinf  10383  zfcndac  10384  pwfseqlem4a  10426  pwfseqlem4  10427  gruina  10583  grothomex  10594  ordpipq  10707  elnpi  10753  genpass  10774  ltprord  10795  reclem2pr  10813  reclem3pr  10814  recexpr  10816  addsrmo  10838  mulsrmo  10839  addsrpr  10840  mulsrpr  10841  ltsosr  10859  mulgt0sr  10870  supsr  10877  ltresr  10905  axpre-lttrn  10931  axpre-mulgt0  10933  prime  12410  peano5uzti  12419  rexuz  12647  ltxr  12860  qbtwnre  12942  xmulneg1  13012  supxr2  13057  ixxval  13096  fzval  13250  preduz  13387  nn0opth2  13995  hashbclem  14173  hashf1lem2  14179  eqwrd  14269  pfxeq  14418  wrd2ind  14445  cshwcsh2id  14550  eqwrds3  14685  cleq1lem  14702  rtrclreclem3  14780  rtrclreclem4  14781  relexpindlem  14783  abslt  15035  absle  15036  lenegsq  15041  abs2difabs  15055  ello12  15234  elo12  15245  o1lo1  15255  rlimuni  15268  lo1resb  15282  o1resb  15284  2clim  15290  rlimcn3  15308  climcn2  15311  addcn2  15312  mulcn2  15314  o1of2  15331  sumeq1  15409  fsum2dlem  15491  modfsummod  15515  prodeq1f  15627  fprod2dlem  15699  nndivdvds  15981  divalg2  16123  smupval  16204  gcdval  16212  gcdass  16264  lcmval  16306  lcmass  16328  rpexp  16436  pythagtriplem2  16527  pythagtrip  16544  vdwapun  16684  0ram  16730  ramub1lem2  16737  pwsle  17212  imasleval  17261  ismre  17308  ismri  17349  iscatd2  17399  dfiso2  17493  isssc  17541  funcpropd  17625  fullpropd  17645  fthres2b  17655  fthres2c  17656  setcsect  17813  cat1lem  17820  cat1  17821  prslem  18025  drsdir  18029  posi  18044  tosso  18146  odudlatb  18252  ipoval  18257  ipolt  18262  dirge  18330  gsumpropd2lem  18372  issgrpv  18386  issgrpn0  18387  mhmpropd  18445  mndind  18475  mgmnsgrpex  18579  issubg3  18782  isga  18906  symgfixelq  19050  psgnfval  19117  psgnval  19124  dprdw  19622  subgdmdprd  19646  drngpropd  20027  issubrg  20033  islmod  20136  lmodlema  20137  lmodprop2d  20194  lsslss  20232  lbspropd  20370  lbsacsbs  20427  znleval  20771  islbs4  21048  islinds3  21050  aspval2  21111  psrbag  21129  pf1ind  21530  mdetunilem4  21773  mdetunilem9  21778  istopg  22053  basis2  22110  tg2  22124  iscld  22187  isnei  22263  isneip  22265  neiptoptop  22291  neiptopnei  22292  neitr  22340  restlp  22343  iscn  22395  cnpval  22396  iscnp  22397  regsep  22494  1stcclb  22604  2ndc1stc  22611  2ndcctbss  22615  2ndcdisj  22616  llyi  22634  nllyi  22635  hausmapdom  22660  locfinnei  22683  comppfsc  22692  elkgen  22696  txbas  22727  txcls  22764  txcnpi  22768  ptpjopn  22772  txdis1cn  22795  txtube  22800  txcmplem1  22801  hausdiag  22805  tx1stc  22810  txkgen  22812  xkococn  22820  elqtop  22857  kqreglem1  22901  elmptrab  22987  isfbas  22989  elflim2  23124  elflim  23131  hauspwpwf1  23147  alexsublem  23204  ghmcnp  23275  qustgplem  23281  tsmssubm  23303  elutop  23394  ustuqtop4  23405  isucn  23439  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  ismet2  23495  imasdsf1olem  23535  blres  23593  elmopn  23604  mopni  23657  neibl  23666  nrmmetd  23739  ngppropd  23802  elcncf  24061  mulc1cncf  24077  elpi1  24217  isclmp  24269  metcld2  24480  pmltpclem1  24621  itg1climres  24888  itg2val  24902  isibl  24939  itgeq1f  24945  itgresr  24952  iblcn  24972  itgfsum  25000  dvreslem  25082  dvfsumlem2  25200  deg1ldg  25266  vieta1  25481  ulm2  25553  sincosq2sgn  25665  sincosq4sgn  25667  efopn  25822  dvdsflsumcom  26346  fsumvma2  26371  logfac2  26374  dchrptlem1  26421  lgsdchrval  26511  2lgslem1a  26548  pntibndlem3  26749  pntlemi  26761  pntleme  26765  pnt3  26769  istrkgld  26829  istrkg2ld  26830  istrkg3ld  26831  axtgsegcon  26834  axtg5seg  26835  axtgpasch  26837  axtgupdim2  26841  legov  26955  islnopp  27109  ishpg  27129  iscgra1  27180  dfcgra2  27200  dfcgrg2  27233  brcgr  27277  brbtwn2  27282  axsegconlem1  27294  axsegcon  27304  axcontlem10  27350  edgssv2  27574  uhgr2edg  27584  isfusgrf1  27696  edgnbusgreu  27743  cplgr3v  27811  vtxdun  27857  upgr2wlk  28045  upgrtrls  28078  upgristrl  28079  upgrf1istrl  28080  2pthnloop  28108  usgr2pth  28141  isclwlke  28154  isclwlkupgr  28155  iswwlksnx  28214  wlknewwlksn  28261  2pthon3v  28317  elwwlks2on  28333  wpthswwlks2on  28335  rusgrnumwwlkl1  28342  rusgrnumwwlkb0  28345  clwwlknp  28410  clwwlkf  28420  erclwwlknsym  28443  erclwwlkntr  28444  clwwlknonwwlknonb  28479  0trl  28495  0spth  28499  0crct  28506  0cycl  28507  upgr4cycl4dv4e  28558  upgriseupth  28580  eupth2lem2  28592  3cyclfrgrrn1  28658  4cycl2vnunb  28663  frgrncvvdeqlem2  28673  frgr2wwlk1  28702  fusgr2wsp2nb  28707  numclwlk1lem1  28742  vciOLD  28932  isvclem  28948  nmoofval  29133  isph  29193  norm3lemt  29523  isch2  29594  cmbr  29955  eigre  30206  eigorth  30209  nmopub  30279  nmfnleub  30296  cvbr  30653  mdbr  30665  dmdbr  30670  chrelat2  30741  mdsymlem2  30775  rexunirn  30849  ifeqeqx  30894  iunrnmptss  30914  funcnvmpt  31013  ressupprn  31033  1stpreima  31048  fpwrelmapffslem  31076  isomnd  31336  archirng  31451  isslmd  31464  slmdlema  31465  orngmul  31511  lindflbs  31583  lindfpropd  31585  idlsrgval  31657  ccfldextdgrr  31751  dya2iocuni  32259  omsfval  32270  elcarsg  32281  itgeq12dv  32302  isrrvv  32419  reprinrn  32607  reprdifc  32616  istrkg2d  32655  axtgupdim2ALTV  32657  brafs  32661  bnj956  32765  bnj1146  32780  bnj18eq1  32916  zltp1ne  33077  isacycgr  33116  kur14  33187  pconncn  33195  cnpconn  33201  txpconn  33203  cvmscbv  33229  cvmcov  33234  cvmsi  33236  cvmsval  33237  cvmopnlem  33249  cvmlift2lem10  33283  cvmlift3lem2  33291  cvmlift3lem6  33295  cvmlift3lem7  33296  cvmlift3lem9  33298  cvmlift3  33299  satf0op  33348  sat1el2xp  33350  satffunlem  33372  dmopab3rexdif  33376  mclsssvlem  33533  mclsind  33541  imaeqsexv  33699  eldm3  33737  opelco3  33758  dfon2lem6  33773  dfon2lem7  33774  dfon2lem8  33775  dfon2  33777  poxp2  33799  xpord3pred  33807  poseq  33811  soseq  33812  sltval  33859  nolt02o  33907  slelttr  33969  nocvxminlem  33981  madebday  34089  sltlpss  34096  elfuns  34226  brsuccf  34252  brofs  34316  5segofs  34317  brifs  34354  ifscgr  34355  brcolinear  34370  lineext  34387  brfs  34390  fscgr  34391  linecgr  34392  btwnconn1lem4  34401  btwnconn1lem8  34405  btwnconn1lem11  34408  btwnconn1lem12  34409  segcon2  34416  brsegle  34419  outsideofeq  34441  funray  34451  funline  34453  fvline  34455  linethru  34464  trer  34514  finminlem  34516  ivthALT  34533  filnetlem4  34579  knoppndvlem21  34721  bj-rabeqd  35116  bj-zfauscl  35121  bj-elgab  35136  bj-imdirvallem  35360  csboprabg  35510  topdifinffinlem  35527  icoreval  35533  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlssretop  35543  pibp19  35594  wl-ax11-lem8  35752  curf  35764  ptrest  35785  poimirlem1  35787  poimirlem13  35799  poimirlem14  35800  poimirlem22  35808  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  heicant  35821  mblfinlem3  35825  mblfinlem4  35826  mbfresfi  35832  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  areacirclem5  35878  cover2  35881  cover2g  35882  fdc  35912  fdc1  35913  heibor1  35977  bfp  35991  rngosn3  36091  drngoi  36118  isdrngo1  36123  isriscg  36151  isfldidl2  36236  islshpat  37038  lcvbr  37042  lshpsmreu  37130  ldual1dim  37187  cvrval  37290  cvrnbtwn3  37297  iscvlat2N  37345  ishlat3N  37375  hlrelat5N  37422  3dim0  37478  llnexatN  37542  islpln5  37556  islvol5  37600  pmapjat1  37874  ltrnu  38142  cdleme02N  38243  cdlemg33b  38728  cdlemg33c  38729  dvhb1dimN  39007  dibelval3  39168  dibopelval3  39169  dib1dim  39186  dibglbN  39187  diblsmopel  39192  dicval  39197  dicopelval  39198  dicelval3  39201  dicelval1sta  39208  dihopelvalcpre  39269  dih1dimatlem  39350  dihpN  39357  dihjatcclem4  39442  lpolsetN  39503  mapdpglem3  39696  hdmapglem7a  39948  fsuppind  40286  fsuppssindlem2  40288  prjspeclsp  40458  mrefg2  40536  mzpclval  40554  eldiophb  40586  eldioph2lem1  40589  eldioph3  40595  lzenom  40599  diophin  40601  eldiophss  40603  diophrex  40604  eq0rabdioph  40605  pellexlem3  40660  elpell1qr  40676  elpell14qr  40678  elpell1234qr  40680  jm2.27  40837  rmydioph  40843  expdiophlem1  40850  expdioph  40852  pw2f1ocnv  40866  hbtlem1  40955  hbtlem7  40957  dgraalem  40977  dgraaub  40980  ifpbi2  41081  inintabd  41194  cnvcnvintabd  41215  cnvintabd  41218  clcnvlem  41238  iunrelexpmin1  41323  uneqsn  41640  k0004lem2  41765  mnuprdlem1  41897  mnuprdlem2  41898  binomcxplemnotnn0  41981  2sbc6g  42040  2sbc5g  42041  iotasbc  42044  dropab1  42072  dropab2  42073  cbvmpo1  42655  disjinfi  42738  dmrelrnrel  42772  mullimc  43164  mullimcf  43171  limsuppnfd  43250  limsuppnf  43259  limsupre2  43273  limsupre2mpt  43278  limsupre3  43281  limsupre3mpt  43282  limsupre3uzlem  43283  fourierdlem42  43697  fourierdlem48  43702  fourierdlem50  43704  fourierdlem51  43705  fourierdlem54  43708  fourierdlem86  43740  ovnval2  44090  ovnsubaddlem1  44115  hoiqssbl  44170  vonicclem2  44229  f1cof1b  44580  f1ocof1ob2  44585  funressnbrafv2  44747  dfatdmfcoafv2  44757  2ffzoeq  44831  fundcmpsurbijinj  44873  ichreuopeq  44936  prproropf1olem4  44969  prprspr2  44981  prprsprreu  44982  prprreueq  44983  reuopreuprim  44989  mgmhmpropd  45350  ismhm0  45370  isrnghm  45461  rngcsect  45549  rngcinv  45550  rngcsectALTV  45561  rngcinvALTV  45562  ringcsect  45600  ringcinv  45601  ringcsectALTV  45624  ringcinvALTV  45625  lmod1  45844  elbigo2  45909  rrx2vlinest  46098  i0oii  46224  io1ii  46225  lubeldm2d  46263  glbeldm2d  46264  functhinc  46337  fullthinc  46338