Theorem anbi1d 642

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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 588	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi12d  643  anbi1  644  pm5.71  1045  cador  1638  drsb1  2527  eleq1w  2846  eleq1d  2848  clelab  2907  rmoeq1f  3406  rabeq  3430  rabeqbidva  3432  rabeqd  3444  rabeqf  3450  alexeqg  3610  reu2eqd  3699  sbc2or  3753  sbc5ALT  3773  rexssOLD  4013  psstr  4062  difin2  4254  r19.28z  4463  dfif6  4490  rabsneq  4608  rexreusng  4645  reurexprg  4670  rabsnifsb  4688  ssunsn2  4793  preq12bg  4818  opeq1  4838  eluni  4875  csbuni  4903  unissb  4906  iuneq12d  4986  disjxun  5107  unopab  5191  mpteq12da  5194  mpteq12f  5196  mpteq12dva  5197  dftr2c  5221  axrep1  5239  axreplem  5240  zfrepclf  5252  axsepgfromrep  5255  axsepg  5258  sepg  5259  zfausclOLD  5261  reusv2lem4  5372  rabxfrd  5388  opthg  5459  otthg  5467  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  opeqsng  5486  euotd  5496  elopabw  5510  pocl  5577  xpeq1  5675  elxpi  5683  vtoclr  5724  opbrop  5759  dmopab2rex  5907  resopab2  6038  rnco  6253  dflim2  6419  dffun2  6546  fun11  6610  feq2  6684  f1eq2  6770  f1eq3  6771  foeq2  6789  brprcneu  6871  brprcneuALT  6872  ssimaexg  6967  dmfco  6977  funcnvmpt  6991  fndmdif  7037  respreima  7061  isoeq5  7319  isoini  7336  isopolem  7343  f1oiso  7349  f1oiso2  7350  imaeqsexvOLD  7361  riotaeqdv  7368  oprabidw  7441  oprabid  7442  oprabv  7470  mpoeq123  7482  mpoeq123dva  7484  0mpo0  7493  eloprabga  7519  resoprab  7528  resoprab2  7529  elrnmpores  7548  ov  7554  ov3  7573  ov6g  7574  ovg  7575  imaeqexov  7648  caoftrn  7715  uniuni  7757  limuni3  7844  elxp4  7915  elxp5  7916  opabex3d  7958  opabex3rd  7959  opabex3  7960  releldmdifi  8038  opiota  8052  eloprabi  8056  mptmpoopabbrd  8074  cnvf1o  8102  frxp  8118  xporderlem  8119  poxp  8120  fnwelem  8123  poxp2  8135  xpord3pred  8144  poseq  8150  soseq  8151  suppimacnv  8166  rexsupp  8174  mpocurryd  8261  smoel2  8346  omeu  8566  oeeui  8584  omabs  8633  omopth  8644  eldifsucnn  8646  qliftel  8794  brecop  8804  eroveu  8806  erov  8808  ecopovtrn  8814  ixpsnf1o  8932  dom2lem  8985  mapsnend  9029  xpsnen  9045  xpassen  9055  pw2f1olem  9065  xpf1o  9123  unxpdom  9215  domunfican  9277  preleqALT  9582  zfinf  9604  cantnfs  9631  brttrcl  9678  ttrclselem2  9691  tcvalg  9701  r0weon  9992  fseqenlem1  10004  acni2  10026  aceq1  10097  aceq0  10098  dfac5lem4  10106  dfac2a  10109  dfac12lem2  10124  cardcf  10230  cfeq0  10235  cfsuc  10236  cff1  10237  cfss  10244  isf32lem5  10336  fin1a2lem6  10384  zfac  10439  brdom7disj  10510  brdom6disj  10511  axrepnd  10574  axunndlem1  10575  axinfnd  10586  axacndlem5  10591  axacnd  10592  zfcndrep  10594  zfcndinf  10598  zfcndac  10599  pwfseqlem4a  10641  pwfseqlem4  10642  gruina  10798  grothomex  10809  ordpipq  10922  elnpi  10968  genpass  10989  ltprord  11010  reclem2pr  11028  reclem3pr  11029  recexpr  11031  addsrmo  11053  mulsrmo  11054  addsrpr  11055  mulsrpr  11056  ltsosr  11074  mulgt0sr  11085  supsr  11092  ltresr  11120  axpre-lttrn  11146  axpre-mulgt0  11148  prime  12672  peano5uzti  12681  rexuz  12917  ltxr  13135  qbtwnre  13220  xmulneg1  13290  supxr2  13335  ixxval  13375  fzval  13532  preduz  13674  nn0opth2  14304  hashbclem  14485  hashf1lem2  14489  eqwrd  14590  pfxeq  14729  wrd2ind  14756  cshwcsh2id  14861  eqwrds3  14994  cleq1lem  15015  rtrclreclem3  15093  rtrclreclem4  15094  relexpindlem  15096  abslt  15362  absle  15363  lenegsq  15368  abs2difabs  15382  ello12  15563  elo12  15574  o1lo1  15584  rlimuni  15597  lo1resb  15611  o1resb  15613  2clim  15619  rlimcn3  15637  climcn2  15640  addcn2  15641  mulcn2  15643  o1of2  15660  sumeq1  15736  fsum2dlem  15817  modfsummod  15842  prodeq1f  15956  prodeq1  15957  fprod2dlem  16030  nndivdvds  16314  divalg2  16458  smupval  16541  gcdval  16549  gcdass  16600  lcmval  16645  lcmass  16667  rpexp  16776  pythagtriplem2  16872  pythagtrip  16889  vdwapun  17029  0ram  17075  ramub1lem2  17082  pwsle  17541  imasleval  17590  ismre  17637  ismri  17682  iscatd2  17732  dfiso2  17824  isssc  17872  funcpropd  17954  fullpropd  17974  fthres2b  17984  fthres2c  17985  setcsect  18141  cat1lem  18148  cat1  18149  prslem  18348  drsdir  18353  posi  18368  tosso  18468  odudlatb  18576  ipoval  18581  ipolt  18586  dirge  18654  gsumpropd2lem  18732  mgmhmpropd  18751  issgrpv  18774  issgrpn0  18775  ismhm0  18843  mhmpropd  18845  mndind  18882  mgmnsgrpex  18988  issubg3  19206  isga  19356  symgfixelq  19498  psgnfval  19565  psgnval  19572  dprdw  20077  subgdmdprd  20101  isomnd  20188  isrnghm  20519  issubrg  20670  resrhm2b  20701  rngcsect  20735  rngcinv  20736  ringcsect  20769  ringcinv  20770  drngpropd  20873  orngmul  20968  islmod  20985  lmodlema  20986  lmodprop2d  21045  lsslss  21082  lbspropd  21220  lbsacsbs  21280  isfieldidl2  21387  znleval  21704  islbs4  21982  islinds3  21984  aspval2  22048  psrbag  22067  pf1ind  22515  mdetunilem4  22772  mdetunilem9  22777  istopg  23052  basis2  23108  tg2  23122  iscld  23184  isnei  23260  isneip  23262  neiptoptop  23288  neiptopnei  23289  neitr  23337  restlp  23340  iscn  23392  cnpval  23393  iscnp  23394  regsep  23491  1stcclb  23601  2ndc1stc  23608  2ndcctbss  23612  2ndcdisj  23613  llyi  23631  nllyi  23632  hausmapdom  23657  locfinnei  23680  comppfsc  23689  elkgen  23693  txbas  23724  txcls  23761  txcnpi  23765  ptpjopn  23769  txdis1cn  23792  txtube  23797  txcmplem1  23798  hausdiag  23802  tx1stc  23807  txkgen  23809  xkococn  23817  elqtop  23854  kqreglem1  23898  elmptrab  23984  isfbas  23986  elflim2  24121  elflim  24128  hauspwpwf1  24144  alexsublem  24201  ghmcnp  24272  qustgplem  24278  tsmssubm  24300  elutop  24390  ustuqtop4  24401  isucn  24434  iscfilu  24444  ispsmet  24461  ismet  24480  isxmet  24481  ismet2  24490  imasdsf1olem  24530  blres  24588  elmopn  24599  mopni  24649  neibl  24658  nrmmetd  24731  ngppropd  24794  elcncf  25048  mulc1cncf  25064  elpi1  25204  isclmp  25256  metcld2  25466  pmltpclem1  25607  itg1climres  25873  itg2val  25887  isibl  25924  itgeq1f  25930  itgeq1fOLD  25931  itgeq1  25932  cbvitgv  25936  itgresr  25938  iblcn  25958  itgfsum  25986  dvreslem  26068  dvfsumlem2  26186  deg1ldg  26249  vieta1  26473  ulm2  26548  sincosq2sgn  26664  sincosq4sgn  26666  efopn  26823  dvdsflsumcom  27352  fsumvma2  27378  logfac2  27381  dchrptlem1  27428  lgsdchrval  27518  2lgslem1a  27555  pntibndlem3  27756  pntlemi  27768  pntleme  27772  pnt3  27776  ltsval  27811  nolt02o  27859  leltstr  27925  nocvxminlem  27947  madebday  28093  ltslpss  28101  addsprop  28169  mulsproplemcbv  28308  mulsproplem1  28309  mulsprop  28323  abslts  28442  eucliddivs  28569  bdayfinbndlem2  28661  z12sge0  28676  istrkgld  28728  istrkg2ld  28729  istrkg3ld  28730  axtgsegcon  28733  axtg5seg  28734  axtgpasch  28736  axtgupdim2  28740  legov  28854  islnopp  29020  ishpg  29041  iscgra1  29121  dfcgra2  29141  dfcgrg2  29180  brprlng  29188  brcgr  29250  brbtwn2  29255  axsegconlem1  29267  axsegcon  29277  axcontlem10  29323  edgssv2  29548  uhgr2edg  29558  isfusgrf1  29670  edgnbusgreu  29717  cplgr3v  29785  vtxdun  29831  upgr2wlk  30016  upgrtrls  30049  upgristrl  30050  upgrf1istrl  30051  dfpth2  30078  2pthnloop  30080  usgr2pth  30113  isclwlke  30126  isclwlkupgr  30127  iswwlksnx  30189  wlknewwlksn  30236  2pthon3v  30292  elwwlks2on  30310  wpthswwlks2on  30313  rusgrnumwwlkl1  30320  rusgrnumwwlkb0  30323  clwwlknp  30388  clwwlkf  30398  erclwwlknsym  30421  erclwwlkntr  30422  clwwlknonwwlknonb  30457  0trl  30473  0spth  30477  0crct  30484  0cycl  30485  upgr4cycl4dv4e  30536  upgriseupth  30558  eupth2lem2  30570  3cyclfrgrrn1  30636  4cycl2vnunb  30641  frgrncvvdeqlem2  30651  frgr2wwlk1  30680  fusgr2wsp2nb  30685  numclwlk1lem1  30720  vciOLD  30913  isvclem  30929  nmoofval  31114  isph  31174  norm3lemt  31504  isch2  31575  cmbr  31936  eigre  32187  eigorth  32190  nmopub  32260  nmfnleub  32277  cvbr  32634  mdbr  32646  dmdbr  32651  chrelat2  32722  mdsymlem2  32756  rexunirn  32838  ifeqeqx  32888  iunrnmptss  32910  fdifsupp  33030  ressupprn  33035  1stpreima  33052  fpwrelmapffslem  33077  archirng  33508  isslmd  33522  slmdlema  33523  urpropd  33550  lindflbs  33692  islbs5  33693  lindfpropd  33695  opprqus0g  33772  idlsrgval  33793  ressply1mon1p  33858  ccfldextdgrr  34062  constrsslem  34131  constrconj  34135  constrlccllem  34143  constrcbvlem  34145  dya2iocuni  34673  omsfval  34684  elcarsg  34695  itgeq12dv  34716  isrrvv  34833  reprinrn  35005  reprdifc  35014  istrkg2d  35053  axtgupdim2ALTV  35055  brafs  35062  bnj956  35165  bnj1146  35179  bnj18eq1  35315  axsepg2  35553  axsepg3  35554  axsepg3ALT  35555  axsepg4  35556  axsepg5  35557  zltp1ne  35601  isacycgr  35637  kur14  35708  pconncn  35716  cnpconn  35722  txpconn  35724  cvmscbv  35750  cvmcov  35755  cvmsi  35757  cvmsval  35758  cvmopnlem  35770  cvmlift2lem10  35804  cvmlift3lem2  35812  cvmlift3lem6  35816  cvmlift3lem7  35817  cvmlift3lem9  35819  cvmlift3  35820  satf0op  35869  sat1el2xp  35871  satffunlem  35893  dmopab3rexdif  35897  mclsssvlem  36054  mclsind  36062  rexxfr3dALT  36131  eldm3  36253  opelco3  36267  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon2  36282  elfuns  36405  lemsuccf  36431  brofs  36497  5segofs  36498  brifs  36535  ifscgr  36536  brcolinear  36551  lineext  36568  brfs  36571  fscgr  36572  linecgr  36573  btwnconn1lem4  36582  btwnconn1lem8  36586  btwnconn1lem11  36589  btwnconn1lem12  36590  segcon2  36597  brsegle  36600  outsideofeq  36622  funray  36632  funline  36634  fvline  36636  linethru  36645  disjeq12dv  36727  prodeq12sdv  36730  itgeq12sdv  36731  cbvitgvw2  36760  cbvitgdavw  36793  cbvitgdavw2  36809  trer  36827  finminlem  36829  ivthALT  36846  filnetlem4  36892  axtco1  36984  axtco1from2  36986  ttcexg  37043  mh-infprim1bi  37057  knoppndvlem21  37121  bj-sepg  37559  bj-elgab  37575  bj-imdirvallem  37824  csboprabg  37976  topdifinffinlem  37993  icoreval  37999  isbasisrelowllem1  38001  isbasisrelowllem2  38002  relowlssretop  38009  pibp19  38060  curf  38249  ptrest  38270  poimirlem1  38272  poimirlem13  38284  poimirlem14  38285  poimirlem22  38293  poimirlem24  38295  poimirlem26  38297  poimirlem27  38298  heicant  38306  mblfinlem3  38310  mblfinlem4  38311  mbfresfi  38317  itg2addnclem3  38324  itg2addnc  38325  itg2gt0cn  38326  areacirclem5  38363  cover2  38366  cover2g  38367  fdc  38396  fdc1  38397  heibor1  38461  bfp  38475  rngosn3  38575  drngoi  38602  isdrngo1  38607  isriscg  38635  isfldidl2  38720  raldmqseu  39014  eldmxrncnvepres  39083  brressn  39180  islshpat  39791  lcvbr  39795  lshpsmreu  39883  ldual1dim  39940  cvrval  40043  cvrnbtwn3  40050  iscvlat2N  40098  ishlat3N  40128  hlrelat5N  40175  3dim0  40231  llnexatN  40295  islpln5  40309  islvol5  40353  pmapjat1  40627  ltrnu  40895  cdleme02N  40996  cdlemg33b  41481  cdlemg33c  41482  dvhb1dimN  41760  dibelval3  41921  dibopelval3  41922  dib1dim  41939  dibglbN  41940  diblsmopel  41945  dicval  41950  dicopelval  41951  dicelval3  41954  dicelval1sta  41961  dihopelvalcpre  42022  dih1dimatlem  42103  dihpN  42110  dihjatcclem4  42195  lpolsetN  42256  mapdpglem3  42449  hdmapglem7a  42701  sticksstones23  42936  exfinfldd  42970  fimgmcyclem  43301  fimgmcyc  43302  fsuppind  43322  fsuppssindlem2  43324  prjspeclsp  43344  mrefg2  43438  mzpclval  43456  eldiophb  43488  eldioph2lem1  43491  eldioph3  43497  lzenom  43501  diophin  43503  eldiophss  43505  diophrex  43506  eq0rabdioph  43507  pellexlem3  43558  elpell1qr  43574  elpell14qr  43576  elpell1234qr  43578  jm2.27  43735  rmydioph  43741  expdiophlem1  43748  expdioph  43750  pw2f1ocnv  43764  hbtlem1  43850  hbtlem7  43852  dgraalem  43872  dgraaub  43875  dflim7  44000  omabs2  44059  tfsconcatfv2  44067  tfsconcat0i  44072  nadd1suc  44119  ifpbi2  44193  inintabd  44305  cnvcnvintabd  44326  cnvintabd  44329  clcnvlem  44349  iunrelexpmin1  44434  uneqsn  44751  k0004lem2  44874  mnuprdlem1  44982  mnuprdlem2  44983  binomcxplemnotnn0  45066  2sbc6g  45125  2sbc5g  45126  iotasbc  45129  dropab1  45156  dropab2  45157  relpeq5  45657  modelaxreplem3  45689  omssaxinf2  45697  brpermmodel  45712  permaxinf2lem  45721  cbvmpo1  45816  r19.28zf  45877  disjinfi  45910  dmrelrnrel  45942  mullimc  46332  mullimcf  46339  limsuppnfd  46416  limsuppnf  46425  limsupre2  46439  limsupre2mpt  46444  limsupre3  46447  limsupre3mpt  46448  limsupre3uzlem  46449  fourierdlem42  46863  fourierdlem48  46868  fourierdlem50  46870  fourierdlem51  46871  fourierdlem54  46874  fourierdlem86  46906  ovnval2  47259  ovnsubaddlem1  47284  hoiqssbl  47339  vonicclem2  47398  f1cof1b  47814  f1ocof1ob2  47819  funressnbrafv2  47981  dfatdmfcoafv2  47991  2ffzoeq  48065  fundcmpsurbijinj  48159  ichreuopeq  48222  prproropf1olem4  48255  prprspr2  48267  prprsprreu  48268  prprreueq  48269  reuopreuprim  48275  nprmmul3  48278  isubgrgrim  48694  grtriprop  48706  isgrtri  48708  opgpgvtx  48820  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem4  48884  grlimedgnedg  48896  rngcsectALTV  49040  rngcinvALTV  49041  ringcsectALTV  49074  ringcinvALTV  49075  lmod1  49272  elbigo2  49332  rrx2vlinest  49521  eloprab1st2nd  49646  i0oii  49698  io1ii  49699  lubeldm2d  49736  glbeldm2d  49737  sectpropdlem  49814  invpropdlem  49816  isopropdlem  49818  uppropd  49959  functhinc  50226  fullthinc  50228