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  1030  cador  1608  drsb1  2500  eleq1w  2824  eleq1d  2826  clelab  2887  rexeqfOLD  3355  rmoeq1OLD  3418  reueq1OLD  3419  rmoeq1f  3424  rabeq  3451  rabeqbidva  3453  rabeqd  3465  rabeqf  3472  cgsex4gOLD  3529  vtocl2gafOLD  3580  vtocl4gaOLD  3587  alexeqg  3651  reu2eqd  3742  sbc2or  3797  sbc5ALT  3817  rexssOLD  4061  psstr  4107  difin2  4301  r19.28z  4498  dfif6  4528  rabsneq  4644  rexreusng  4679  reurexprg  4704  rabsnifsb  4722  ssunsn2  4827  preq12bg  4853  opeq1  4873  eluni  4910  csbuni  4936  unissb  4939  iuneq12d  5021  disjxun  5141  unopab  5224  mpteq12da  5227  mpteq12f  5230  mpteq12dva  5231  dftr2c  5262  axrep1  5280  axreplem  5281  zfrepclf  5291  axsepgfromrep  5294  axsepg  5297  zfauscl  5298  reusv2lem4  5401  rabxfrd  5417  opthg  5482  otthg  5490  copsexgw  5495  copsexg  5496  opeqsng  5508  euotd  5518  elopabw  5531  pocl  5600  xpeq1  5699  elxpi  5707  vtoclr  5748  opbrop  5783  dmopab2rex  5928  resopab2  6054  dflim2  6441  dffun2  6571  fun11  6640  feq2  6717  f1eq2  6800  f1eq3  6801  foeq2  6817  brprcneu  6896  brprcneuALT  6897  ssimaexg  6995  dmfco  7005  fndmdif  7062  respreima  7086  isoeq5  7341  isoini  7358  isopolem  7365  f1oiso  7371  f1oiso2  7372  imaeqsexvOLD  7383  riotaeqdv  7389  oprabidw  7462  oprabid  7463  oprabv  7493  mpoeq123  7505  mpoeq123dva  7507  0mpo0  7516  eloprabga  7542  resoprab  7551  resoprab2  7552  elrnmpores  7571  ov  7577  ov3  7596  ov6g  7597  ovg  7598  imaeqexov  7671  caoftrn  7738  uniuni  7782  limuni3  7873  elxp4  7944  elxp5  7945  opabex3d  7990  opabex3rd  7991  opabex3  7992  releldmdifi  8070  opiota  8084  eloprabi  8088  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabbrdOLDOLD  8108  cnvf1o  8136  frxp  8151  xporderlem  8152  poxp  8153  fnwelem  8156  poxp2  8168  xpord3pred  8177  poseq  8183  soseq  8184  suppimacnv  8199  rexsupp  8207  mpocurryd  8294  smoel2  8403  omeu  8623  oeeui  8640  omabs  8689  omopth  8700  eldifsucnn  8702  qliftel  8840  brecop  8850  eroveu  8852  erov  8854  ecopovtrn  8860  ixpsnf1o  8978  dom2lem  9032  mapsnend  9076  xpsnen  9095  xpassen  9106  pw2f1olem  9116  xpf1o  9179  unxpdom  9289  domunfican  9361  preleqALT  9657  zfinf  9679  cantnfs  9706  brttrcl  9753  ttrclselem2  9766  tcvalg  9778  r0weon  10052  fseqenlem1  10064  acni2  10086  aceq1  10157  aceq0  10158  dfac5lem4  10166  dfac2a  10170  dfac12lem2  10185  cardcf  10292  cfeq0  10296  cfsuc  10297  cff1  10298  cfss  10305  isf32lem5  10397  fin1a2lem6  10445  zfac  10500  brdom7disj  10571  brdom6disj  10572  axrepnd  10634  axunndlem1  10635  axinfnd  10646  axacndlem5  10651  axacnd  10652  zfcndrep  10654  zfcndinf  10658  zfcndac  10659  pwfseqlem4a  10701  pwfseqlem4  10702  gruina  10858  grothomex  10869  ordpipq  10982  elnpi  11028  genpass  11049  ltprord  11070  reclem2pr  11088  reclem3pr  11089  recexpr  11091  addsrmo  11113  mulsrmo  11114  addsrpr  11115  mulsrpr  11116  ltsosr  11134  mulgt0sr  11145  supsr  11152  ltresr  11180  axpre-lttrn  11206  axpre-mulgt0  11208  prime  12699  peano5uzti  12708  rexuz  12940  ltxr  13157  qbtwnre  13241  xmulneg1  13311  supxr2  13356  ixxval  13395  fzval  13549  preduz  13690  nn0opth2  14311  hashbclem  14491  hashf1lem2  14495  eqwrd  14595  pfxeq  14734  wrd2ind  14761  cshwcsh2id  14867  eqwrds3  15000  cleq1lem  15021  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  abslt  15353  absle  15354  lenegsq  15359  abs2difabs  15373  ello12  15552  elo12  15563  o1lo1  15573  rlimuni  15586  lo1resb  15600  o1resb  15602  2clim  15608  rlimcn3  15626  climcn2  15629  addcn2  15630  mulcn2  15632  o1of2  15649  sumeq1  15725  fsum2dlem  15806  modfsummod  15830  prodeq1f  15942  prodeq1  15943  fprod2dlem  16016  nndivdvds  16299  divalg2  16442  smupval  16525  gcdval  16533  gcdass  16584  lcmval  16629  lcmass  16651  rpexp  16759  pythagtriplem2  16855  pythagtrip  16872  vdwapun  17012  0ram  17058  ramub1lem2  17065  pwsle  17537  imasleval  17586  ismre  17633  ismri  17674  iscatd2  17724  dfiso2  17816  isssc  17864  funcpropd  17947  fullpropd  17967  fthres2b  17977  fthres2c  17978  setcsect  18134  cat1lem  18141  cat1  18142  prslem  18343  drsdir  18348  posi  18363  tosso  18464  odudlatb  18570  ipoval  18575  ipolt  18580  dirge  18648  gsumpropd2lem  18692  mgmhmpropd  18711  issgrpv  18734  issgrpn0  18735  ismhm0  18803  mhmpropd  18805  mndind  18841  mgmnsgrpex  18944  issubg3  19162  isga  19309  symgfixelq  19451  psgnfval  19518  psgnval  19525  dprdw  20030  subgdmdprd  20054  isrnghm  20441  issubrg  20571  resrhm2b  20602  rngcsect  20636  rngcinv  20637  ringcsect  20670  ringcinv  20671  drngpropd  20769  islmod  20862  lmodlema  20863  lmodprop2d  20922  lsslss  20959  lbspropd  21098  lbsacsbs  21158  znleval  21573  islbs4  21852  islinds3  21854  aspval2  21918  psrbag  21937  pf1ind  22359  mdetunilem4  22621  mdetunilem9  22626  istopg  22901  basis2  22958  tg2  22972  iscld  23035  isnei  23111  isneip  23113  neiptoptop  23139  neiptopnei  23140  neitr  23188  restlp  23191  iscn  23243  cnpval  23244  iscnp  23245  regsep  23342  1stcclb  23452  2ndc1stc  23459  2ndcctbss  23463  2ndcdisj  23464  llyi  23482  nllyi  23483  hausmapdom  23508  locfinnei  23531  comppfsc  23540  elkgen  23544  txbas  23575  txcls  23612  txcnpi  23616  ptpjopn  23620  txdis1cn  23643  txtube  23648  txcmplem1  23649  hausdiag  23653  tx1stc  23658  txkgen  23660  xkococn  23668  elqtop  23705  kqreglem1  23749  elmptrab  23835  isfbas  23837  elflim2  23972  elflim  23979  hauspwpwf1  23995  alexsublem  24052  ghmcnp  24123  qustgplem  24129  tsmssubm  24151  elutop  24242  ustuqtop4  24253  isucn  24287  iscfilu  24297  ispsmet  24314  ismet  24333  isxmet  24334  ismet2  24343  imasdsf1olem  24383  blres  24441  elmopn  24452  mopni  24505  neibl  24514  nrmmetd  24587  ngppropd  24650  elcncf  24915  mulc1cncf  24931  elpi1  25078  isclmp  25130  metcld2  25341  pmltpclem1  25483  itg1climres  25749  itg2val  25763  isibl  25800  itgeq1f  25806  itgeq1fOLD  25807  itgeq1  25808  cbvitgv  25812  itgresr  25814  iblcn  25834  itgfsum  25862  dvreslem  25944  dvfsumlem2  26067  dvfsumlem2OLD  26068  deg1ldg  26131  vieta1  26354  ulm2  26428  sincosq2sgn  26541  sincosq4sgn  26543  efopn  26700  dvdsflsumcom  27231  fsumvma2  27258  logfac2  27261  dchrptlem1  27308  lgsdchrval  27398  2lgslem1a  27435  pntibndlem3  27636  pntlemi  27648  pntleme  27652  pnt3  27656  sltval  27692  nolt02o  27740  slelttr  27802  nocvxminlem  27822  madebday  27938  sltlpss  27945  addsprop  28009  mulsproplemcbv  28141  mulsproplem1  28142  mulsprop  28156  absslt  28273  istrkgld  28467  istrkg2ld  28468  istrkg3ld  28469  axtgsegcon  28472  axtg5seg  28473  axtgpasch  28475  axtgupdim2  28479  legov  28593  islnopp  28747  ishpg  28767  iscgra1  28818  dfcgra2  28838  dfcgrg2  28871  brcgr  28915  brbtwn2  28920  axsegconlem1  28932  axsegcon  28942  axcontlem10  28988  edgssv2  29215  uhgr2edg  29225  isfusgrf1  29337  edgnbusgreu  29384  cplgr3v  29452  vtxdun  29499  upgr2wlk  29686  upgrtrls  29719  upgristrl  29720  upgrf1istrl  29721  dfpth2  29749  2pthnloop  29751  usgr2pth  29784  isclwlke  29797  isclwlkupgr  29798  iswwlksnx  29860  wlknewwlksn  29907  2pthon3v  29963  elwwlks2on  29979  wpthswwlks2on  29981  rusgrnumwwlkl1  29988  rusgrnumwwlkb0  29991  clwwlknp  30056  clwwlkf  30066  erclwwlknsym  30089  erclwwlkntr  30090  clwwlknonwwlknonb  30125  0trl  30141  0spth  30145  0crct  30152  0cycl  30153  upgr4cycl4dv4e  30204  upgriseupth  30226  eupth2lem2  30238  3cyclfrgrrn1  30304  4cycl2vnunb  30309  frgrncvvdeqlem2  30319  frgr2wwlk1  30348  fusgr2wsp2nb  30353  numclwlk1lem1  30388  vciOLD  30580  isvclem  30596  nmoofval  30781  isph  30841  norm3lemt  31171  isch2  31242  cmbr  31603  eigre  31854  eigorth  31857  nmopub  31927  nmfnleub  31944  cvbr  32301  mdbr  32313  dmdbr  32318  chrelat2  32389  mdsymlem2  32423  rexunirn  32511  ifeqeqx  32555  iunrnmptss  32578  funcnvmpt  32677  fdifsupp  32694  ressupprn  32699  1stpreima  32716  fpwrelmapffslem  32743  isomnd  33078  archirng  33195  isslmd  33208  slmdlema  33209  urpropd  33236  orngmul  33333  lindflbs  33407  islbs5  33408  lindfpropd  33410  opprqus0g  33518  idlsrgval  33531  ressply1mon1p  33593  ccfldextdgrr  33722  constrsslem  33782  constrconj  33786  dya2iocuni  34285  omsfval  34296  elcarsg  34307  itgeq12dv  34328  isrrvv  34445  reprinrn  34633  reprdifc  34642  istrkg2d  34681  axtgupdim2ALTV  34683  brafs  34687  bnj956  34790  bnj1146  34805  bnj18eq1  34941  axsepg2  35096  axsepg2ALT  35097  zltp1ne  35115  isacycgr  35150  kur14  35221  pconncn  35229  cnpconn  35235  txpconn  35237  cvmscbv  35263  cvmcov  35268  cvmsi  35270  cvmsval  35271  cvmopnlem  35283  cvmlift2lem10  35317  cvmlift3lem2  35325  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  cvmlift3  35333  satf0op  35382  sat1el2xp  35384  satffunlem  35406  dmopab3rexdif  35410  mclsssvlem  35567  mclsind  35575  rexxfr3dALT  35644  eldm3  35761  opelco3  35775  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  elfuns  35916  brsuccf  35942  brofs  36006  5segofs  36007  brifs  36044  ifscgr  36045  brcolinear  36060  lineext  36077  brfs  36080  fscgr  36081  linecgr  36082  btwnconn1lem4  36091  btwnconn1lem8  36095  btwnconn1lem11  36098  btwnconn1lem12  36099  segcon2  36106  brsegle  36109  outsideofeq  36131  funray  36141  funline  36143  fvline  36145  linethru  36154  disjeq12dv  36216  prodeq12sdv  36219  itgeq12sdv  36220  cbvitgvw2  36249  cbvitgdavw  36282  cbvitgdavw2  36298  trer  36317  finminlem  36319  ivthALT  36336  filnetlem4  36382  knoppndvlem21  36533  bj-zfauscl  36925  bj-elgab  36940  bj-imdirvallem  37181  csboprabg  37331  topdifinffinlem  37348  icoreval  37354  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlssretop  37364  pibp19  37415  wl-ax11-lem8  37593  curf  37605  ptrest  37626  poimirlem1  37628  poimirlem13  37640  poimirlem14  37641  poimirlem22  37649  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  heicant  37662  mblfinlem3  37666  mblfinlem4  37667  mbfresfi  37673  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  areacirclem5  37719  cover2  37722  cover2g  37723  fdc  37752  fdc1  37753  heibor1  37817  bfp  37831  rngosn3  37931  drngoi  37958  isdrngo1  37963  isriscg  37991  isfldidl2  38076  brressn  38442  islshpat  39018  lcvbr  39022  lshpsmreu  39110  ldual1dim  39167  cvrval  39270  cvrnbtwn3  39277  iscvlat2N  39325  ishlat3N  39355  hlrelat5N  39403  3dim0  39459  llnexatN  39523  islpln5  39537  islvol5  39581  pmapjat1  39855  ltrnu  40123  cdleme02N  40224  cdlemg33b  40709  cdlemg33c  40710  dvhb1dimN  40988  dibelval3  41149  dibopelval3  41150  dib1dim  41167  dibglbN  41168  diblsmopel  41173  dicval  41178  dicopelval  41179  dicelval3  41182  dicelval1sta  41189  dihopelvalcpre  41250  dih1dimatlem  41331  dihpN  41338  dihjatcclem4  41423  lpolsetN  41484  mapdpglem3  41677  hdmapglem7a  41929  sticksstones23  42170  exfinfldd  42204  fimgmcyclem  42543  fimgmcyc  42544  fsuppind  42600  fsuppssindlem2  42602  prjspeclsp  42622  mrefg2  42718  mzpclval  42736  eldiophb  42768  eldioph2lem1  42771  eldioph3  42777  lzenom  42781  diophin  42783  eldiophss  42785  diophrex  42786  eq0rabdioph  42787  pellexlem3  42842  elpell1qr  42858  elpell14qr  42860  elpell1234qr  42862  jm2.27  43020  rmydioph  43026  expdiophlem1  43033  expdioph  43035  pw2f1ocnv  43049  hbtlem1  43135  hbtlem7  43137  dgraalem  43157  dgraaub  43160  dflim7  43286  omabs2  43345  tfsconcatfv2  43353  tfsconcat0i  43358  nadd1suc  43405  ifpbi2  43480  inintabd  43592  cnvcnvintabd  43613  cnvintabd  43616  clcnvlem  43636  iunrelexpmin1  43721  uneqsn  44038  k0004lem2  44161  mnuprdlem1  44291  mnuprdlem2  44292  binomcxplemnotnn0  44375  2sbc6g  44434  2sbc5g  44435  iotasbc  44438  dropab1  44466  dropab2  44467  relpeq5  44969  modelaxreplem3  44997  omssaxinf2  45005  cbvmpo1  45103  r19.28zf  45164  disjinfi  45197  dmrelrnrel  45231  mullimc  45631  mullimcf  45638  limsuppnfd  45717  limsuppnf  45726  limsupre2  45740  limsupre2mpt  45745  limsupre3  45748  limsupre3mpt  45749  limsupre3uzlem  45750  fourierdlem42  46164  fourierdlem48  46169  fourierdlem50  46171  fourierdlem51  46172  fourierdlem54  46175  fourierdlem86  46207  ovnval2  46560  ovnsubaddlem1  46585  hoiqssbl  46640  vonicclem2  46699  f1cof1b  47089  f1ocof1ob2  47094  funressnbrafv2  47256  dfatdmfcoafv2  47266  2ffzoeq  47339  fundcmpsurbijinj  47397  ichreuopeq  47460  prproropf1olem4  47493  prprspr2  47505  prprsprreu  47506  prprreueq  47507  reuopreuprim  47513  isubgrgrim  47897  grtriprop  47908  isgrtri  47910  opgpgvtx  48010  rngcsectALTV  48191  rngcinvALTV  48192  ringcsectALTV  48225  ringcinvALTV  48226  lmod1  48409  elbigo2  48473  rrx2vlinest  48662  i0oii  48817  io1ii  48818  lubeldm2d  48855  glbeldm2d  48856  functhinc  49097  fullthinc  49099