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  3328  rmoeq1OLD  3386  reueq1OLD  3387  rmoeq1f  3392  rabeq  3417  rabeqbidva  3419  rabeqd  3431  rabeqf  3437  cgsex4gOLD  3492  vtocl2gafOLD  3543  vtocl4gaOLD  3550  alexeqg  3614  reu2eqd  3704  sbc2or  3759  sbc5ALT  3779  rexssOLD  4021  psstr  4066  difin2  4260  r19.28z  4457  dfif6  4487  rabsneq  4604  rexreusng  4639  reurexprg  4664  rabsnifsb  4682  ssunsn2  4787  preq12bg  4813  opeq1  4833  eluni  4870  csbuni  4896  unissb  4899  iuneq12d  4981  disjxun  5100  unopab  5182  mpteq12da  5185  mpteq12f  5187  mpteq12dva  5188  dftr2c  5212  axrep1  5230  axreplem  5231  zfrepclf  5241  axsepgfromrep  5244  axsepg  5247  zfauscl  5248  reusv2lem4  5351  rabxfrd  5367  opthg  5432  otthg  5440  copsexgw  5445  copsexg  5446  opeqsng  5458  euotd  5468  elopabw  5481  pocl  5547  xpeq1  5645  elxpi  5653  vtoclr  5694  opbrop  5728  dmopab2rex  5871  resopab2  5996  dflim2  6378  dffun2  6509  fun11  6574  feq2  6649  f1eq2  6734  f1eq3  6735  foeq2  6751  brprcneu  6830  brprcneuALT  6831  ssimaexg  6929  dmfco  6939  fndmdif  6996  respreima  7020  isoeq5  7278  isoini  7295  isopolem  7302  f1oiso  7308  f1oiso2  7309  imaeqsexvOLD  7320  riotaeqdv  7327  oprabidw  7400  oprabid  7401  oprabv  7429  mpoeq123  7441  mpoeq123dva  7443  0mpo0  7452  eloprabga  7478  resoprab  7487  resoprab2  7488  elrnmpores  7507  ov  7513  ov3  7532  ov6g  7533  ovg  7534  imaeqexov  7607  caoftrn  7674  uniuni  7718  limuni3  7808  elxp4  7878  elxp5  7879  opabex3d  7923  opabex3rd  7924  opabex3  7925  releldmdifi  8003  opiota  8017  eloprabi  8021  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  cnvf1o  8067  frxp  8082  xporderlem  8083  poxp  8084  fnwelem  8087  poxp2  8099  xpord3pred  8108  poseq  8114  soseq  8115  suppimacnv  8130  rexsupp  8138  mpocurryd  8225  smoel2  8309  omeu  8526  oeeui  8543  omabs  8592  omopth  8603  eldifsucnn  8605  qliftel  8750  brecop  8760  eroveu  8762  erov  8764  ecopovtrn  8770  ixpsnf1o  8888  dom2lem  8940  mapsnend  8984  xpsnen  9002  xpassen  9012  pw2f1olem  9022  xpf1o  9080  unxpdom  9176  domunfican  9248  preleqALT  9546  zfinf  9568  cantnfs  9595  brttrcl  9642  ttrclselem2  9655  tcvalg  9667  r0weon  9941  fseqenlem1  9953  acni2  9975  aceq1  10046  aceq0  10047  dfac5lem4  10055  dfac2a  10059  dfac12lem2  10074  cardcf  10181  cfeq0  10185  cfsuc  10186  cff1  10187  cfss  10194  isf32lem5  10286  fin1a2lem6  10334  zfac  10389  brdom7disj  10460  brdom6disj  10461  axrepnd  10523  axunndlem1  10524  axinfnd  10535  axacndlem5  10540  axacnd  10541  zfcndrep  10543  zfcndinf  10547  zfcndac  10548  pwfseqlem4a  10590  pwfseqlem4  10591  gruina  10747  grothomex  10758  ordpipq  10871  elnpi  10917  genpass  10938  ltprord  10959  reclem2pr  10977  reclem3pr  10978  recexpr  10980  addsrmo  11002  mulsrmo  11003  addsrpr  11004  mulsrpr  11005  ltsosr  11023  mulgt0sr  11034  supsr  11041  ltresr  11069  axpre-lttrn  11095  axpre-mulgt0  11097  prime  12591  peano5uzti  12600  rexuz  12833  ltxr  13051  qbtwnre  13135  xmulneg1  13205  supxr2  13250  ixxval  13290  fzval  13446  preduz  13587  nn0opth2  14213  hashbclem  14393  hashf1lem2  14397  eqwrd  14498  pfxeq  14637  wrd2ind  14664  cshwcsh2id  14770  eqwrds3  14903  cleq1lem  14924  rtrclreclem3  15002  rtrclreclem4  15003  relexpindlem  15005  abslt  15257  absle  15258  lenegsq  15263  abs2difabs  15277  ello12  15458  elo12  15469  o1lo1  15479  rlimuni  15492  lo1resb  15506  o1resb  15508  2clim  15514  rlimcn3  15532  climcn2  15535  addcn2  15536  mulcn2  15538  o1of2  15555  sumeq1  15631  fsum2dlem  15712  modfsummod  15736  prodeq1f  15848  prodeq1  15849  fprod2dlem  15922  nndivdvds  16207  divalg2  16351  smupval  16434  gcdval  16442  gcdass  16493  lcmval  16538  lcmass  16560  rpexp  16668  pythagtriplem2  16764  pythagtrip  16781  vdwapun  16921  0ram  16967  ramub1lem2  16974  pwsle  17431  imasleval  17480  ismre  17527  ismri  17568  iscatd2  17618  dfiso2  17710  isssc  17758  funcpropd  17840  fullpropd  17860  fthres2b  17870  fthres2c  17871  setcsect  18027  cat1lem  18034  cat1  18035  prslem  18234  drsdir  18239  posi  18254  tosso  18354  odudlatb  18460  ipoval  18465  ipolt  18470  dirge  18538  gsumpropd2lem  18582  mgmhmpropd  18601  issgrpv  18624  issgrpn0  18625  ismhm0  18693  mhmpropd  18695  mndind  18731  mgmnsgrpex  18834  issubg3  19052  isga  19199  symgfixelq  19339  psgnfval  19406  psgnval  19413  dprdw  19918  subgdmdprd  19942  isrnghm  20326  issubrg  20456  resrhm2b  20487  rngcsect  20521  rngcinv  20522  ringcsect  20555  ringcinv  20556  drngpropd  20654  islmod  20746  lmodlema  20747  lmodprop2d  20806  lsslss  20843  lbspropd  20982  lbsacsbs  21042  znleval  21440  islbs4  21717  islinds3  21719  aspval2  21783  psrbag  21802  pf1ind  22218  mdetunilem4  22478  mdetunilem9  22483  istopg  22758  basis2  22814  tg2  22828  iscld  22890  isnei  22966  isneip  22968  neiptoptop  22994  neiptopnei  22995  neitr  23043  restlp  23046  iscn  23098  cnpval  23099  iscnp  23100  regsep  23197  1stcclb  23307  2ndc1stc  23314  2ndcctbss  23318  2ndcdisj  23319  llyi  23337  nllyi  23338  hausmapdom  23363  locfinnei  23386  comppfsc  23395  elkgen  23399  txbas  23430  txcls  23467  txcnpi  23471  ptpjopn  23475  txdis1cn  23498  txtube  23503  txcmplem1  23504  hausdiag  23508  tx1stc  23513  txkgen  23515  xkococn  23523  elqtop  23560  kqreglem1  23604  elmptrab  23690  isfbas  23692  elflim2  23827  elflim  23834  hauspwpwf1  23850  alexsublem  23907  ghmcnp  23978  qustgplem  23984  tsmssubm  24006  elutop  24097  ustuqtop4  24108  isucn  24141  iscfilu  24151  ispsmet  24168  ismet  24187  isxmet  24188  ismet2  24197  imasdsf1olem  24237  blres  24295  elmopn  24306  mopni  24356  neibl  24365  nrmmetd  24438  ngppropd  24501  elcncf  24758  mulc1cncf  24774  elpi1  24921  isclmp  24973  metcld2  25183  pmltpclem1  25325  itg1climres  25591  itg2val  25605  isibl  25642  itgeq1f  25648  itgeq1fOLD  25649  itgeq1  25650  cbvitgv  25654  itgresr  25656  iblcn  25676  itgfsum  25704  dvreslem  25786  dvfsumlem2  25909  dvfsumlem2OLD  25910  deg1ldg  25973  vieta1  26196  ulm2  26270  sincosq2sgn  26384  sincosq4sgn  26386  efopn  26543  dvdsflsumcom  27074  fsumvma2  27101  logfac2  27104  dchrptlem1  27151  lgsdchrval  27241  2lgslem1a  27278  pntibndlem3  27479  pntlemi  27491  pntleme  27495  pnt3  27499  sltval  27535  nolt02o  27583  slelttr  27645  nocvxminlem  27665  madebday  27787  sltlpss  27795  addsprop  27859  mulsproplemcbv  27994  mulsproplem1  27995  mulsprop  28009  absslt  28127  eucliddivs  28241  zs12ge0  28318  istrkgld  28362  istrkg2ld  28363  istrkg3ld  28364  axtgsegcon  28367  axtg5seg  28368  axtgpasch  28370  axtgupdim2  28374  legov  28488  islnopp  28642  ishpg  28662  iscgra1  28713  dfcgra2  28733  dfcgrg2  28766  brcgr  28803  brbtwn2  28808  axsegconlem1  28820  axsegcon  28830  axcontlem10  28876  edgssv2  29101  uhgr2edg  29111  isfusgrf1  29223  edgnbusgreu  29270  cplgr3v  29338  vtxdun  29385  upgr2wlk  29570  upgrtrls  29603  upgristrl  29604  upgrf1istrl  29605  dfpth2  29632  2pthnloop  29634  usgr2pth  29667  isclwlke  29680  isclwlkupgr  29681  iswwlksnx  29743  wlknewwlksn  29790  2pthon3v  29846  elwwlks2on  29862  wpthswwlks2on  29864  rusgrnumwwlkl1  29871  rusgrnumwwlkb0  29874  clwwlknp  29939  clwwlkf  29949  erclwwlknsym  29972  erclwwlkntr  29973  clwwlknonwwlknonb  30008  0trl  30024  0spth  30028  0crct  30035  0cycl  30036  upgr4cycl4dv4e  30087  upgriseupth  30109  eupth2lem2  30121  3cyclfrgrrn1  30187  4cycl2vnunb  30192  frgrncvvdeqlem2  30202  frgr2wwlk1  30231  fusgr2wsp2nb  30236  numclwlk1lem1  30271  vciOLD  30463  isvclem  30479  nmoofval  30664  isph  30724  norm3lemt  31054  isch2  31125  cmbr  31486  eigre  31737  eigorth  31740  nmopub  31810  nmfnleub  31827  cvbr  32184  mdbr  32196  dmdbr  32201  chrelat2  32272  mdsymlem2  32306  rexunirn  32394  ifeqeqx  32444  iunrnmptss  32467  funcnvmpt  32564  fdifsupp  32581  ressupprn  32586  1stpreima  32603  fpwrelmapffslem  32628  isomnd  32988  archirng  33115  isslmd  33128  slmdlema  33129  urpropd  33156  orngmul  33254  lindflbs  33323  islbs5  33324  lindfpropd  33326  opprqus0g  33434  idlsrgval  33447  ressply1mon1p  33510  ccfldextdgrr  33640  constrsslem  33704  constrconj  33708  constrlccllem  33716  constrcbvlem  33718  dya2iocuni  34247  omsfval  34258  elcarsg  34269  itgeq12dv  34290  isrrvv  34407  reprinrn  34582  reprdifc  34591  istrkg2d  34630  axtgupdim2ALTV  34632  brafs  34636  bnj956  34739  bnj1146  34754  bnj18eq1  34890  axsepg2  35045  axsepg2ALT  35046  zltp1ne  35070  isacycgr  35105  kur14  35176  pconncn  35184  cnpconn  35190  txpconn  35192  cvmscbv  35218  cvmcov  35223  cvmsi  35225  cvmsval  35226  cvmopnlem  35238  cvmlift2lem10  35272  cvmlift3lem2  35280  cvmlift3lem6  35284  cvmlift3lem7  35285  cvmlift3lem9  35287  cvmlift3  35288  satf0op  35337  sat1el2xp  35339  satffunlem  35361  dmopab3rexdif  35365  mclsssvlem  35522  mclsind  35530  rexxfr3dALT  35599  eldm3  35721  opelco3  35735  dfon2lem6  35749  dfon2lem7  35750  dfon2lem8  35751  dfon2  35753  elfuns  35876  brsuccf  35902  brofs  35966  5segofs  35967  brifs  36004  ifscgr  36005  brcolinear  36020  lineext  36037  brfs  36040  fscgr  36041  linecgr  36042  btwnconn1lem4  36051  btwnconn1lem8  36055  btwnconn1lem11  36058  btwnconn1lem12  36059  segcon2  36066  brsegle  36069  outsideofeq  36091  funray  36101  funline  36103  fvline  36105  linethru  36114  disjeq12dv  36176  prodeq12sdv  36179  itgeq12sdv  36180  cbvitgvw2  36209  cbvitgdavw  36242  cbvitgdavw2  36258  trer  36277  finminlem  36279  ivthALT  36296  filnetlem4  36342  knoppndvlem21  36493  bj-zfauscl  36885  bj-elgab  36900  bj-imdirvallem  37141  csboprabg  37291  topdifinffinlem  37308  icoreval  37314  isbasisrelowllem1  37316  isbasisrelowllem2  37317  relowlssretop  37324  pibp19  37375  wl-ax11-lem8  37553  curf  37565  ptrest  37586  poimirlem1  37588  poimirlem13  37600  poimirlem14  37601  poimirlem22  37609  poimirlem24  37611  poimirlem26  37613  poimirlem27  37614  heicant  37622  mblfinlem3  37626  mblfinlem4  37627  mbfresfi  37633  itg2addnclem3  37640  itg2addnc  37641  itg2gt0cn  37642  areacirclem5  37679  cover2  37682  cover2g  37683  fdc  37712  fdc1  37713  heibor1  37777  bfp  37791  rngosn3  37891  drngoi  37918  isdrngo1  37923  isriscg  37951  isfldidl2  38036  eldmxrncnvepres  38369  brressn  38405  islshpat  38983  lcvbr  38987  lshpsmreu  39075  ldual1dim  39132  cvrval  39235  cvrnbtwn3  39242  iscvlat2N  39290  ishlat3N  39320  hlrelat5N  39368  3dim0  39424  llnexatN  39488  islpln5  39502  islvol5  39546  pmapjat1  39820  ltrnu  40088  cdleme02N  40189  cdlemg33b  40674  cdlemg33c  40675  dvhb1dimN  40953  dibelval3  41114  dibopelval3  41115  dib1dim  41132  dibglbN  41133  diblsmopel  41138  dicval  41143  dicopelval  41144  dicelval3  41147  dicelval1sta  41154  dihopelvalcpre  41215  dih1dimatlem  41296  dihpN  41303  dihjatcclem4  41388  lpolsetN  41449  mapdpglem3  41642  hdmapglem7a  41894  sticksstones23  42130  exfinfldd  42164  fimgmcyclem  42494  fimgmcyc  42495  fsuppind  42551  fsuppssindlem2  42553  prjspeclsp  42573  mrefg2  42668  mzpclval  42686  eldiophb  42718  eldioph2lem1  42721  eldioph3  42727  lzenom  42731  diophin  42733  eldiophss  42735  diophrex  42736  eq0rabdioph  42737  pellexlem3  42792  elpell1qr  42808  elpell14qr  42810  elpell1234qr  42812  jm2.27  42970  rmydioph  42976  expdiophlem1  42983  expdioph  42985  pw2f1ocnv  42999  hbtlem1  43085  hbtlem7  43087  dgraalem  43107  dgraaub  43110  dflim7  43235  omabs2  43294  tfsconcatfv2  43302  tfsconcat0i  43307  nadd1suc  43354  ifpbi2  43429  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  clcnvlem  43585  iunrelexpmin1  43670  uneqsn  43987  k0004lem2  44110  mnuprdlem1  44234  mnuprdlem2  44235  binomcxplemnotnn0  44318  2sbc6g  44377  2sbc5g  44378  iotasbc  44381  dropab1  44409  dropab2  44410  relpeq5  44911  modelaxreplem3  44943  omssaxinf2  44951  brpermmodel  44966  permaxinf2lem  44975  cbvmpo1  45065  r19.28zf  45126  disjinfi  45159  dmrelrnrel  45193  mullimc  45587  mullimcf  45594  limsuppnfd  45673  limsuppnf  45682  limsupre2  45696  limsupre2mpt  45701  limsupre3  45704  limsupre3mpt  45705  limsupre3uzlem  45706  fourierdlem42  46120  fourierdlem48  46125  fourierdlem50  46127  fourierdlem51  46128  fourierdlem54  46131  fourierdlem86  46163  ovnval2  46516  ovnsubaddlem1  46541  hoiqssbl  46596  vonicclem2  46655  f1cof1b  47051  f1ocof1ob2  47056  funressnbrafv2  47218  dfatdmfcoafv2  47228  2ffzoeq  47301  fundcmpsurbijinj  47384  ichreuopeq  47447  prproropf1olem4  47480  prprspr2  47492  prprsprreu  47493  prprreueq  47494  reuopreuprim  47500  isubgrgrim  47902  grtriprop  47913  isgrtri  47915  opgpgvtx  48019  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem4  48082  rngcsectALTV  48236  rngcinvALTV  48237  ringcsectALTV  48270  ringcinvALTV  48271  lmod1  48454  elbigo2  48514  rrx2vlinest  48703  eloprab1st2nd  48829  i0oii  48881  io1ii  48882  lubeldm2d  48919  glbeldm2d  48920  sectpropdlem  48998  invpropdlem  49000  isopropdlem  49002  uppropd  49143  functhinc  49410  fullthinc  49412