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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anbi12d  632  anbi1  633  pm5.71  1024  cador  1609  drsb1  2535  eleq1w  2897  eleq1d  2899  rexeqf  3400  reueq1f  3401  rmoeq1f  3402  reueq1  3409  rmoeq1  3410  rabeqf  3483  rabeqi  3484  rabeq  3485  vtocl2gaf  3578  vtocl4ga  3582  alexeqg  3646  elrabi  3677  reu2eqd  3729  sbc2or  3783  sbc5  3802  rexss  4040  psstr  4083  ineq1OLD  4184  difin2  4268  r19.28z  4445  rexreusng  4619  reurexprg  4642  rabsnifsb  4660  ssunsn2  4762  preq12bg  4786  opeq1  4805  eluni  4843  csbuni  4869  disjxun  5066  mpteq12f  5151  axrep1  5193  axreplem  5194  zfrepclf  5200  axsepgfromrep  5203  axsepg  5206  zfauscl  5207  reusv2lem4  5304  rabxfrd  5320  opthg  5371  otthg  5379  copsexgw  5383  copsexg  5384  opeqsng  5395  euotd  5405  elopab  5416  pocl  5483  xpeq1  5571  elxpi  5579  vtoclr  5617  opbrop  5650  dmopab2rex  5788  resopab2  5906  dflim2  6249  fun11  6430  feq2  6498  f1eq2  6573  f1eq3  6574  foeq2  6589  brprcneu  6664  ssimaexg  6751  dmfco  6759  fndmdif  6814  respreima  6838  isoeq5  7076  isoini  7093  isopolem  7100  f1oiso  7106  f1oiso2  7107  riotaeqdv  7117  oprabidw  7189  oprabid  7190  oprabv  7216  mpoeq123  7228  mpoeq123dva  7230  eloprabga  7263  resoprab  7272  resoprab2  7273  elrnmpores  7290  ov  7296  ov3  7313  ov6g  7314  ovg  7315  caoftrn  7446  uniuni  7486  limuni3  7569  elxp4  7629  elxp5  7630  opabex3d  7668  opabex3rd  7669  opabex3  7670  releldmdifi  7746  opiota  7759  eloprabi  7763  mptmpoopabbrd  7780  cnvf1o  7808  frxp  7822  xporderlem  7823  poxp  7824  fnwelem  7827  suppimacnv  7843  rexsupp  7850  mpocurryd  7937  smoel2  8002  omeu  8213  oeeui  8230  omabs  8276  omopth  8287  qliftel  8382  brecop  8392  eroveu  8394  erov  8396  ecopovtrn  8402  ixpsnf1o  8504  dom2lem  8551  mapsnend  8590  xpsnen  8603  xpassen  8613  pw2f1olem  8623  xpf1o  8681  unxpdom  8727  domunfican  8793  preleqALT  9082  zfinf  9104  cantnfs  9131  tcvalg  9182  r0weon  9440  fseqenlem1  9452  acni2  9474  aceq1  9545  aceq0  9546  dfac2a  9557  dfac12lem2  9572  cardcf  9676  cfeq0  9680  cfsuc  9681  cff1  9682  cfss  9689  isf32lem5  9781  fin1a2lem6  9829  zfac  9884  brdom7disj  9955  brdom6disj  9956  axrepnd  10018  axunndlem1  10019  axinfnd  10030  axacndlem5  10035  axacnd  10036  zfcndrep  10038  zfcndinf  10042  zfcndac  10043  pwfseqlem4a  10085  pwfseqlem4  10086  gruina  10242  grothomex  10253  ordpipq  10366  elnpi  10412  genpass  10433  ltprord  10454  reclem2pr  10472  reclem3pr  10473  recexpr  10475  addsrmo  10497  mulsrmo  10498  addsrpr  10499  mulsrpr  10500  ltsosr  10518  mulgt0sr  10529  supsr  10536  ltresr  10564  axpre-lttrn  10590  axpre-mulgt0  10592  prime  12066  peano5uzti  12075  rexuz  12301  ltxr  12513  qbtwnre  12595  xmulneg1  12665  supxr2  12710  ixxval  12749  fzval  12897  preduz  13032  nn0opth2  13635  hashbclem  13813  hashf1lem2  13817  eqwrd  13911  pfxeq  14060  wrd2ind  14087  cshwcsh2id  14192  eqwrds3  14327  cleq1lem  14344  rtrclreclem3  14421  rtrclreclem4  14422  relexpindlem  14424  abslt  14676  absle  14677  lenegsq  14682  abs2difabs  14696  ello12  14875  elo12  14886  o1lo1  14896  rlimuni  14909  lo1resb  14923  o1resb  14925  2clim  14931  rlimcn2  14949  climcn2  14951  addcn2  14952  mulcn2  14954  o1of2  14971  sumeq1  15047  fsum2dlem  15127  modfsummod  15151  prodeq1f  15264  fprod2dlem  15336  nndivdvds  15618  divalg2  15758  smupval  15839  gcdval  15847  gcdass  15897  lcmval  15938  lcmass  15960  rpexp  16066  pythagtriplem2  16156  pythagtrip  16173  vdwapun  16312  0ram  16358  ramub1lem2  16365  pwsle  16767  imasleval  16816  ismre  16863  ismri  16904  iscatd2  16954  dfiso2  17044  isssc  17092  funcpropd  17172  fullpropd  17192  fthres2b  17202  fthres2c  17203  setcsect  17351  prslem  17543  drsdir  17547  posi  17562  tosso  17648  ipoval  17766  ipolt  17771  odudlatb  17808  dirge  17849  gsumpropd2lem  17891  issgrpv  17905  issgrpn0  17906  mhmpropd  17964  mndind  17994  mgmnsgrpex  18098  issubg3  18299  isga  18423  symgfixelq  18563  psgnfval  18630  psgnval  18637  dprdw  19134  subgdmdprd  19158  drngpropd  19531  issubrg  19537  islmod  19640  lmodlema  19641  lmodprop2d  19698  lsslss  19735  lbspropd  19873  lbsacsbs  19930  aspval2  20129  psrbag  20146  pf1ind  20520  znleval  20703  islbs4  20978  islinds3  20980  mdetunilem4  21226  mdetunilem9  21231  istopg  21505  basis2  21561  tg2  21575  iscld  21637  isnei  21713  isneip  21715  neiptoptop  21741  neiptopnei  21742  neitr  21790  restlp  21793  iscn  21845  cnpval  21846  iscnp  21847  regsep  21944  1stcclb  22054  2ndc1stc  22061  2ndcctbss  22065  2ndcdisj  22066  llyi  22084  nllyi  22085  hausmapdom  22110  locfinnei  22133  comppfsc  22142  elkgen  22146  txbas  22177  txcls  22214  txcnpi  22218  ptpjopn  22222  txdis1cn  22245  txtube  22250  txcmplem1  22251  hausdiag  22255  tx1stc  22260  txkgen  22262  xkococn  22270  elqtop  22307  kqreglem1  22351  elmptrab  22437  isfbas  22439  elflim2  22574  elflim  22581  hauspwpwf1  22597  alexsublem  22654  ghmcnp  22725  qustgplem  22731  tsmssubm  22753  elutop  22844  ustuqtop4  22855  isucn  22889  iscfilu  22899  ispsmet  22916  ismet  22935  isxmet  22936  ismet2  22945  imasdsf1olem  22985  blres  23043  elmopn  23054  mopni  23104  neibl  23113  nrmmetd  23186  ngppropd  23248  elcncf  23499  mulc1cncf  23515  elpi1  23651  isclmp  23703  metcld2  23912  pmltpclem1  24051  itg1climres  24317  itg2val  24331  isibl  24368  itgeq1f  24374  itgresr  24381  iblcn  24401  itgfsum  24429  dvreslem  24509  dvfsumlem2  24626  deg1ldg  24688  vieta1  24903  ulm2  24975  sincosq2sgn  25087  sincosq4sgn  25089  efopn  25243  dvdsflsumcom  25767  fsumvma2  25792  logfac2  25795  dchrptlem1  25842  lgsdchrval  25932  2lgslem1a  25969  pntibndlem3  26170  pntlemi  26182  pntleme  26186  pnt3  26190  istrkgld  26247  istrkg2ld  26248  istrkg3ld  26249  axtgsegcon  26252  axtg5seg  26253  axtgpasch  26255  axtgupdim2  26259  legov  26373  islnopp  26527  ishpg  26547  iscgra1  26598  dfcgra2  26618  dfcgrg2  26651  brcgr  26688  brbtwn2  26693  axsegconlem1  26705  axsegcon  26715  axcontlem10  26761  edgssv2  26982  uhgr2edg  26992  isfusgrf1  27104  edgnbusgreu  27151  cplgr3v  27219  vtxdun  27265  upgr2wlk  27452  upgrtrls  27485  upgristrl  27486  upgrf1istrl  27487  2pthnloop  27514  usgr2pth  27547  isclwlke  27560  isclwlkupgr  27561  iswwlksnx  27620  wlknewwlksn  27667  wwlksnfiOLD  27687  2pthon3v  27724  elwwlks2on  27740  wpthswwlks2on  27742  rusgrnumwwlkl1  27749  rusgrnumwwlkb0  27752  clwwlknp  27817  clwwlkf  27828  erclwwlknsym  27851  erclwwlkntr  27852  clwwlknonwwlknonb  27887  0trl  27903  0spth  27907  0crct  27914  0cycl  27915  upgr4cycl4dv4e  27966  upgriseupth  27988  eupth2lem2  28000  3cyclfrgrrn1  28066  4cycl2vnunb  28071  frgrncvvdeqlem2  28081  frgr2wwlk1  28110  fusgr2wsp2nb  28115  numclwlk1lem1  28150  vciOLD  28340  isvclem  28356  nmoofval  28541  isph  28601  norm3lemt  28931  isch2  29002  cmbr  29363  eigre  29614  eigorth  29617  nmopub  29687  nmfnleub  29704  cvbr  30061  mdbr  30073  dmdbr  30078  chrelat2  30149  mdsymlem2  30183  rexunirn  30258  ifeqeqx  30299  iunrnmptss  30319  funcnvmpt  30414  1stpreima  30444  fpwrelmapffslem  30470  isomnd  30704  archirng  30819  isslmd  30832  slmdlema  30833  orngmul  30878  lindflbs  30942  lindfpropd  30944  ccfldextdgrr  31059  dya2iocuni  31543  omsfval  31554  elcarsg  31565  itgeq12dv  31586  isrrvv  31703  reprinrn  31891  reprdifc  31900  istrkg2d  31939  axtgupdim2ALTV  31941  brafs  31945  bnj956  32050  bnj1146  32065  bnj18eq1  32201  zltp1ne  32350  isacycgr  32394  kur14  32465  pconncn  32473  cnpconn  32479  txpconn  32481  cvmscbv  32507  cvmcov  32512  cvmsi  32514  cvmsval  32515  cvmopnlem  32527  cvmlift2lem10  32561  cvmlift3lem2  32569  cvmlift3lem6  32573  cvmlift3lem7  32574  cvmlift3lem9  32576  cvmlift3  32577  satf0op  32626  sat1el2xp  32628  satffunlem  32650  dmopab3rexdif  32654  mclsssvlem  32811  mclsind  32819  eldm3  32999  opelco3  33020  dfon2lem6  33035  dfon2lem7  33036  dfon2lem8  33037  dfon2  33039  poseq  33097  soseq  33098  sltval  33156  nolt02o  33201  slelttr  33238  nocvxminlem  33249  elfuns  33378  brsuccf  33404  brofs  33468  5segofs  33469  brifs  33506  ifscgr  33507  brcolinear  33522  lineext  33539  brfs  33542  fscgr  33543  linecgr  33544  btwnconn1lem4  33553  btwnconn1lem8  33557  btwnconn1lem11  33560  btwnconn1lem12  33561  segcon2  33568  brsegle  33571  outsideofeq  33593  funray  33603  funline  33605  fvline  33607  linethru  33616  trer  33666  finminlem  33668  ivthALT  33685  filnetlem4  33731  knoppndvlem21  33873  bj-rabeqd  34240  bj-zfauscl  34245  bj-imdirval  34474  csboprabg  34613  topdifinffinlem  34630  icoreval  34636  isbasisrelowllem1  34638  isbasisrelowllem2  34639  relowlssretop  34646  pibp19  34697  wl-ax11-lem8  34826  curf  34872  ptrest  34893  poimirlem1  34895  poimirlem13  34907  poimirlem14  34908  poimirlem22  34916  poimirlem24  34918  poimirlem26  34920  poimirlem27  34921  heicant  34929  mblfinlem3  34933  mblfinlem4  34934  mbfresfi  34940  itg2addnclem3  34947  itg2addnc  34948  itg2gt0cn  34949  areacirclem5  34988  cover2  34991  cover2g  34992  fdc  35022  fdc1  35023  heibor1  35090  bfp  35104  rngosn3  35204  drngoi  35231  isdrngo1  35236  isriscg  35264  isfldidl2  35349  islshpat  36155  lcvbr  36159  lshpsmreu  36247  ldual1dim  36304  cvrval  36407  cvrnbtwn3  36414  iscvlat2N  36462  ishlat3N  36492  hlrelat5N  36539  3dim0  36595  llnexatN  36659  islpln5  36673  islvol5  36717  pmapjat1  36991  ltrnu  37259  cdleme02N  37360  cdlemg33b  37845  cdlemg33c  37846  dvhb1dimN  38124  dibelval3  38285  dibopelval3  38286  dib1dim  38303  dibglbN  38304  diblsmopel  38309  dicval  38314  dicopelval  38315  dicelval3  38318  dicelval1sta  38325  dihopelvalcpre  38386  dih1dimatlem  38467  dihpN  38474  dihjatcclem4  38559  lpolsetN  38620  mapdpglem3  38813  hdmapglem7a  39065  prjspeclsp  39269  mrefg2  39311  mzpclval  39329  eldiophb  39361  eldioph2lem1  39364  eldioph3  39370  lzenom  39374  diophin  39376  eldiophss  39378  diophrex  39379  eq0rabdioph  39380  pellexlem3  39435  elpell1qr  39451  elpell14qr  39453  elpell1234qr  39455  jm2.27  39612  rmydioph  39618  expdiophlem1  39625  expdioph  39627  pw2f1ocnv  39641  hbtlem1  39730  hbtlem7  39732  dgraalem  39752  dgraaub  39755  ifpbi2  39839  inintabd  39946  cnvcnvintabd  39967  cnvintabd  39970  clcnvlem  39990  iunrelexpmin1  40060  uneqsn  40380  k0004lem2  40505  mnuprdlem1  40615  mnuprdlem2  40616  binomcxplemnotnn0  40695  2sbc6g  40754  2sbc5g  40755  iotasbc  40758  dropab1  40786  dropab2  40787  cbvmpo1  41371  disjinfi  41461  dmrelrnrel  41497  mullimc  41904  mullimcf  41911  limsuppnfd  41990  limsuppnf  41999  limsupre2  42013  limsupre2mpt  42018  limsupre3  42021  limsupre3mpt  42022  limsupre3uzlem  42023  fourierdlem42  42441  fourierdlem48  42446  fourierdlem50  42448  fourierdlem51  42449  fourierdlem54  42452  fourierdlem86  42484  ovnval2  42834  ovnsubaddlem1  42859  hoiqssbl  42914  vonicclem2  42973  funressnbrafv2  43450  dfatdmfcoafv2  43460  2ffzoeq  43535  fundcmpsurbijinj  43577  ichreuopeq  43642  prproropf1olem4  43675  prprspr2  43687  prprsprreu  43688  prprreueq  43689  reuopreuprim  43695  mgmhmpropd  44059  ismhm0  44079  isrnghm  44170  rngcsect  44258  rngcinv  44259  rngcsectALTV  44270  rngcinvALTV  44271  ringcsect  44309  ringcinv  44310  ringcsectALTV  44333  ringcinvALTV  44334  lmod1  44554  elbigo2  44619  rrx2vlinest  44735