Theorem anbi1d 629

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi12d  630  anbi1  631  pm5.71  1024  cador  1611  drsb1  2499  eleq1w  2821  eleq1d  2823  clelab  2882  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  reueq1  3335  rmoeq1  3336  rabeqf  3405  rabeqiOLD  3407  rabeq  3408  cgsex4g  3466  vtocl2gaf  3505  vtocl4ga  3510  alexeqg  3573  elrabiOLD  3612  reu2eqd  3666  sbc2or  3720  sbc5ALT  3740  rexss  3988  psstr  4035  difin2  4222  r19.28z  4425  dfif6  4459  rexreusng  4612  reurexprg  4637  rabsnifsb  4655  ssunsn2  4757  preq12bg  4781  opeq1  4801  eluni  4839  csbuni  4867  disjxun  5068  unopab  5152  mpteq12da  5155  mpteq12f  5158  mpteq12dva  5159  axrep1  5206  axreplem  5207  zfrepclf  5213  axsepgfromrep  5216  axsepg  5219  zfauscl  5220  reusv2lem4  5319  rabxfrd  5335  opthg  5386  otthg  5394  copsexgw  5398  copsexg  5399  opeqsng  5411  euotd  5421  elopab  5433  pocl  5501  poclOLD  5502  xpeq1  5594  elxpi  5602  vtoclr  5641  opbrop  5674  dmopab2rex  5815  resopab2  5933  dflim2  6307  fun11  6492  feq2  6566  f1eq2  6650  f1eq3  6651  foeq2  6669  brprcneu  6747  fvprc  6748  ssimaexg  6836  dmfco  6846  fndmdif  6901  respreima  6925  isoeq5  7172  isoini  7189  isopolem  7196  f1oiso  7202  f1oiso2  7203  riotaeqdv  7213  oprabidw  7286  oprabid  7287  oprabv  7313  mpoeq123  7325  mpoeq123dva  7327  0mpo0  7336  eloprabga  7360  eloprabgaOLD  7361  resoprab  7370  resoprab2  7371  elrnmpores  7389  ov  7395  ov3  7413  ov6g  7414  ovg  7415  caoftrn  7549  uniuni  7590  limuni3  7674  elxp4  7743  elxp5  7744  opabex3d  7781  opabex3rd  7782  opabex3  7783  releldmdifi  7859  opiota  7872  eloprabi  7876  mptmpoopabbrd  7894  cnvf1o  7922  frxp  7938  xporderlem  7939  poxp  7940  fnwelem  7943  suppimacnv  7961  rexsupp  7969  mpocurryd  8056  smoel2  8165  omeu  8378  oeeui  8395  omabs  8441  omopth  8452  qliftel  8547  brecop  8557  eroveu  8559  erov  8561  ecopovtrn  8567  ixpsnf1o  8684  dom2lem  8735  mapsnend  8780  xpsnen  8796  xpassen  8806  pw2f1olem  8816  xpf1o  8875  unxpdom  8959  domunfican  9017  preleqALT  9305  zfinf  9327  cantnfs  9354  tcvalg  9427  r0weon  9699  fseqenlem1  9711  acni2  9733  aceq1  9804  aceq0  9805  dfac2a  9816  dfac12lem2  9831  cardcf  9939  cfeq0  9943  cfsuc  9944  cff1  9945  cfss  9952  isf32lem5  10044  fin1a2lem6  10092  zfac  10147  brdom7disj  10218  brdom6disj  10219  axrepnd  10281  axunndlem1  10282  axinfnd  10293  axacndlem5  10298  axacnd  10299  zfcndrep  10301  zfcndinf  10305  zfcndac  10306  pwfseqlem4a  10348  pwfseqlem4  10349  gruina  10505  grothomex  10516  ordpipq  10629  elnpi  10675  genpass  10696  ltprord  10717  reclem2pr  10735  reclem3pr  10736  recexpr  10738  addsrmo  10760  mulsrmo  10761  addsrpr  10762  mulsrpr  10763  ltsosr  10781  mulgt0sr  10792  supsr  10799  ltresr  10827  axpre-lttrn  10853  axpre-mulgt0  10855  prime  12331  peano5uzti  12340  rexuz  12567  ltxr  12780  qbtwnre  12862  xmulneg1  12932  supxr2  12977  ixxval  13016  fzval  13170  preduz  13307  nn0opth2  13914  hashbclem  14092  hashf1lem2  14098  eqwrd  14188  pfxeq  14337  wrd2ind  14364  cshwcsh2id  14469  eqwrds3  14604  cleq1lem  14621  rtrclreclem3  14699  rtrclreclem4  14700  relexpindlem  14702  abslt  14954  absle  14955  lenegsq  14960  abs2difabs  14974  ello12  15153  elo12  15164  o1lo1  15174  rlimuni  15187  lo1resb  15201  o1resb  15203  2clim  15209  rlimcn3  15227  climcn2  15230  addcn2  15231  mulcn2  15233  o1of2  15250  sumeq1  15328  fsum2dlem  15410  modfsummod  15434  prodeq1f  15546  fprod2dlem  15618  nndivdvds  15900  divalg2  16042  smupval  16123  gcdval  16131  gcdass  16183  lcmval  16225  lcmass  16247  rpexp  16355  pythagtriplem2  16446  pythagtrip  16463  vdwapun  16603  0ram  16649  ramub1lem2  16656  pwsle  17120  imasleval  17169  ismre  17216  ismri  17257  iscatd2  17307  dfiso2  17401  isssc  17449  funcpropd  17532  fullpropd  17552  fthres2b  17562  fthres2c  17563  setcsect  17720  cat1lem  17727  cat1  17728  prslem  17931  drsdir  17935  posi  17950  tosso  18052  odudlatb  18158  ipoval  18163  ipolt  18168  dirge  18236  gsumpropd2lem  18278  issgrpv  18292  issgrpn0  18293  mhmpropd  18351  mndind  18381  mgmnsgrpex  18485  issubg3  18688  isga  18812  symgfixelq  18956  psgnfval  19023  psgnval  19030  dprdw  19528  subgdmdprd  19552  drngpropd  19933  issubrg  19939  islmod  20042  lmodlema  20043  lmodprop2d  20100  lsslss  20138  lbspropd  20276  lbsacsbs  20333  znleval  20674  islbs4  20949  islinds3  20951  aspval2  21012  psrbag  21030  pf1ind  21431  mdetunilem4  21672  mdetunilem9  21677  istopg  21952  basis2  22009  tg2  22023  iscld  22086  isnei  22162  isneip  22164  neiptoptop  22190  neiptopnei  22191  neitr  22239  restlp  22242  iscn  22294  cnpval  22295  iscnp  22296  regsep  22393  1stcclb  22503  2ndc1stc  22510  2ndcctbss  22514  2ndcdisj  22515  llyi  22533  nllyi  22534  hausmapdom  22559  locfinnei  22582  comppfsc  22591  elkgen  22595  txbas  22626  txcls  22663  txcnpi  22667  ptpjopn  22671  txdis1cn  22694  txtube  22699  txcmplem1  22700  hausdiag  22704  tx1stc  22709  txkgen  22711  xkococn  22719  elqtop  22756  kqreglem1  22800  elmptrab  22886  isfbas  22888  elflim2  23023  elflim  23030  hauspwpwf1  23046  alexsublem  23103  ghmcnp  23174  qustgplem  23180  tsmssubm  23202  elutop  23293  ustuqtop4  23304  isucn  23338  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  ismet2  23394  imasdsf1olem  23434  blres  23492  elmopn  23503  mopni  23554  neibl  23563  nrmmetd  23636  ngppropd  23699  elcncf  23958  mulc1cncf  23974  elpi1  24114  isclmp  24166  metcld2  24376  pmltpclem1  24517  itg1climres  24784  itg2val  24798  isibl  24835  itgeq1f  24841  itgresr  24848  iblcn  24868  itgfsum  24896  dvreslem  24978  dvfsumlem2  25096  deg1ldg  25162  vieta1  25377  ulm2  25449  sincosq2sgn  25561  sincosq4sgn  25563  efopn  25718  dvdsflsumcom  26242  fsumvma2  26267  logfac2  26270  dchrptlem1  26317  lgsdchrval  26407  2lgslem1a  26444  pntibndlem3  26645  pntlemi  26657  pntleme  26661  pnt3  26665  istrkgld  26724  istrkg2ld  26725  istrkg3ld  26726  axtgsegcon  26729  axtg5seg  26730  axtgpasch  26732  axtgupdim2  26736  legov  26850  islnopp  27004  ishpg  27024  iscgra1  27075  dfcgra2  27095  dfcgrg2  27128  brcgr  27171  brbtwn2  27176  axsegconlem1  27188  axsegcon  27198  axcontlem10  27244  edgssv2  27468  uhgr2edg  27478  isfusgrf1  27590  edgnbusgreu  27637  cplgr3v  27705  vtxdun  27751  upgr2wlk  27938  upgrtrls  27971  upgristrl  27972  upgrf1istrl  27973  2pthnloop  28000  usgr2pth  28033  isclwlke  28046  isclwlkupgr  28047  iswwlksnx  28106  wlknewwlksn  28153  2pthon3v  28209  elwwlks2on  28225  wpthswwlks2on  28227  rusgrnumwwlkl1  28234  rusgrnumwwlkb0  28237  clwwlknp  28302  clwwlkf  28312  erclwwlknsym  28335  erclwwlkntr  28336  clwwlknonwwlknonb  28371  0trl  28387  0spth  28391  0crct  28398  0cycl  28399  upgr4cycl4dv4e  28450  upgriseupth  28472  eupth2lem2  28484  3cyclfrgrrn1  28550  4cycl2vnunb  28555  frgrncvvdeqlem2  28565  frgr2wwlk1  28594  fusgr2wsp2nb  28599  numclwlk1lem1  28634  vciOLD  28824  isvclem  28840  nmoofval  29025  isph  29085  norm3lemt  29415  isch2  29486  cmbr  29847  eigre  30098  eigorth  30101  nmopub  30171  nmfnleub  30188  cvbr  30545  mdbr  30557  dmdbr  30562  chrelat2  30633  mdsymlem2  30667  rexunirn  30741  ifeqeqx  30786  iunrnmptss  30806  funcnvmpt  30906  ressupprn  30926  1stpreima  30941  fpwrelmapffslem  30969  isomnd  31229  archirng  31344  isslmd  31357  slmdlema  31358  orngmul  31404  lindflbs  31476  lindfpropd  31478  idlsrgval  31550  ccfldextdgrr  31644  dya2iocuni  32150  omsfval  32161  elcarsg  32172  itgeq12dv  32193  isrrvv  32310  reprinrn  32498  reprdifc  32507  istrkg2d  32546  axtgupdim2ALTV  32548  brafs  32552  bnj956  32656  bnj1146  32671  bnj18eq1  32807  zltp1ne  32968  isacycgr  33007  kur14  33078  pconncn  33086  cnpconn  33092  txpconn  33094  cvmscbv  33120  cvmcov  33125  cvmsi  33127  cvmsval  33128  cvmopnlem  33140  cvmlift2lem10  33174  cvmlift3lem2  33182  cvmlift3lem6  33186  cvmlift3lem7  33187  cvmlift3lem9  33189  cvmlift3  33190  satf0op  33239  sat1el2xp  33241  satffunlem  33263  dmopab3rexdif  33267  mclsssvlem  33424  mclsind  33432  imaeqsexv  33593  eldifsucnn  33597  eldm3  33634  opelco3  33655  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  dfon2  33674  brttrcl  33699  ttrclselem2  33712  poxp2  33717  xpord3pred  33725  poseq  33729  soseq  33730  sltval  33777  nolt02o  33825  slelttr  33887  nocvxminlem  33899  madebday  34007  sltlpss  34014  elfuns  34144  brsuccf  34170  brofs  34234  5segofs  34235  brifs  34272  ifscgr  34273  brcolinear  34288  lineext  34305  brfs  34308  fscgr  34309  linecgr  34310  btwnconn1lem4  34319  btwnconn1lem8  34323  btwnconn1lem11  34326  btwnconn1lem12  34327  segcon2  34334  brsegle  34337  outsideofeq  34359  funray  34369  funline  34371  fvline  34373  linethru  34382  trer  34432  finminlem  34434  ivthALT  34451  filnetlem4  34497  knoppndvlem21  34639  bj-rabeqd  35034  bj-zfauscl  35039  bj-elgab  35054  bj-imdirvallem  35278  csboprabg  35428  topdifinffinlem  35445  icoreval  35451  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  pibp19  35512  wl-ax11-lem8  35670  curf  35682  ptrest  35703  poimirlem1  35705  poimirlem13  35717  poimirlem14  35718  poimirlem22  35726  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  heicant  35739  mblfinlem3  35743  mblfinlem4  35744  mbfresfi  35750  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  areacirclem5  35796  cover2  35799  cover2g  35800  fdc  35830  fdc1  35831  heibor1  35895  bfp  35909  rngosn3  36009  drngoi  36036  isdrngo1  36041  isriscg  36069  isfldidl2  36154  islshpat  36958  lcvbr  36962  lshpsmreu  37050  ldual1dim  37107  cvrval  37210  cvrnbtwn3  37217  iscvlat2N  37265  ishlat3N  37295  hlrelat5N  37342  3dim0  37398  llnexatN  37462  islpln5  37476  islvol5  37520  pmapjat1  37794  ltrnu  38062  cdleme02N  38163  cdlemg33b  38648  cdlemg33c  38649  dvhb1dimN  38927  dibelval3  39088  dibopelval3  39089  dib1dim  39106  dibglbN  39107  diblsmopel  39112  dicval  39117  dicopelval  39118  dicelval3  39121  dicelval1sta  39128  dihopelvalcpre  39189  dih1dimatlem  39270  dihpN  39277  dihjatcclem4  39362  lpolsetN  39423  mapdpglem3  39616  hdmapglem7a  39868  fsuppind  40202  fsuppssindlem2  40204  prjspeclsp  40372  mrefg2  40445  mzpclval  40463  eldiophb  40495  eldioph2lem1  40498  eldioph3  40504  lzenom  40508  diophin  40510  eldiophss  40512  diophrex  40513  eq0rabdioph  40514  pellexlem3  40569  elpell1qr  40585  elpell14qr  40587  elpell1234qr  40589  jm2.27  40746  rmydioph  40752  expdiophlem1  40759  expdioph  40761  pw2f1ocnv  40775  hbtlem1  40864  hbtlem7  40866  dgraalem  40886  dgraaub  40889  ifpbi2  40972  inintabd  41076  cnvcnvintabd  41097  cnvintabd  41100  clcnvlem  41120  iunrelexpmin1  41205  uneqsn  41522  k0004lem2  41647  mnuprdlem1  41779  mnuprdlem2  41780  binomcxplemnotnn0  41863  2sbc6g  41922  2sbc5g  41923  iotasbc  41926  dropab1  41954  dropab2  41955  cbvmpo1  42537  disjinfi  42620  dmrelrnrel  42654  mullimc  43047  mullimcf  43054  limsuppnfd  43133  limsuppnf  43142  limsupre2  43156  limsupre2mpt  43161  limsupre3  43164  limsupre3mpt  43165  limsupre3uzlem  43166  fourierdlem42  43580  fourierdlem48  43585  fourierdlem50  43587  fourierdlem51  43588  fourierdlem54  43591  fourierdlem86  43623  ovnval2  43973  ovnsubaddlem1  43998  hoiqssbl  44053  vonicclem2  44112  f1cof1b  44456  f1ocof1ob2  44461  funressnbrafv2  44623  dfatdmfcoafv2  44633  2ffzoeq  44708  fundcmpsurbijinj  44750  ichreuopeq  44813  prproropf1olem4  44846  prprspr2  44858  prprsprreu  44859  prprreueq  44860  reuopreuprim  44866  mgmhmpropd  45227  ismhm0  45247  isrnghm  45338  rngcsect  45426  rngcinv  45427  rngcsectALTV  45438  rngcinvALTV  45439  ringcsect  45477  ringcinv  45478  ringcsectALTV  45501  ringcinvALTV  45502  lmod1  45721  elbigo2  45786  rrx2vlinest  45975  i0oii  46101  io1ii  46102  lubeldm2d  46140  glbeldm2d  46141  functhinc  46214  fullthinc  46215