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  2494  eleq1w  2812  eleq1d  2814  clelab  2874  rexeqfOLD  3333  rmoeq1OLD  3392  reueq1OLD  3393  rmoeq1f  3398  rabeq  3423  rabeqbidva  3425  rabeqd  3437  rabeqf  3443  cgsex4gOLD  3498  vtocl2gafOLD  3549  vtocl4gaOLD  3556  alexeqg  3620  reu2eqd  3710  sbc2or  3765  sbc5ALT  3785  rexssOLD  4027  psstr  4073  difin2  4267  r19.28z  4464  dfif6  4494  rabsneq  4611  rexreusng  4646  reurexprg  4671  rabsnifsb  4689  ssunsn2  4794  preq12bg  4820  opeq1  4840  eluni  4877  csbuni  4903  unissb  4906  iuneq12d  4988  disjxun  5108  unopab  5190  mpteq12da  5193  mpteq12f  5195  mpteq12dva  5196  dftr2c  5220  axrep1  5238  axreplem  5239  zfrepclf  5249  axsepgfromrep  5252  axsepg  5255  zfauscl  5256  reusv2lem4  5359  rabxfrd  5375  opthg  5440  otthg  5448  copsexgw  5453  copsexg  5454  opeqsng  5466  euotd  5476  elopabw  5489  pocl  5557  xpeq1  5655  elxpi  5663  vtoclr  5704  opbrop  5739  dmopab2rex  5884  resopab2  6010  dflim2  6393  dffun2  6524  fun11  6593  feq2  6670  f1eq2  6755  f1eq3  6756  foeq2  6772  brprcneu  6851  brprcneuALT  6852  ssimaexg  6950  dmfco  6960  fndmdif  7017  respreima  7041  isoeq5  7299  isoini  7316  isopolem  7323  f1oiso  7329  f1oiso2  7330  imaeqsexvOLD  7341  riotaeqdv  7348  oprabidw  7421  oprabid  7422  oprabv  7452  mpoeq123  7464  mpoeq123dva  7466  0mpo0  7475  eloprabga  7501  resoprab  7510  resoprab2  7511  elrnmpores  7530  ov  7536  ov3  7555  ov6g  7556  ovg  7557  imaeqexov  7630  caoftrn  7697  uniuni  7741  limuni3  7831  elxp4  7901  elxp5  7902  opabex3d  7947  opabex3rd  7948  opabex3  7949  releldmdifi  8027  opiota  8041  eloprabi  8045  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabbrdOLDOLD  8065  cnvf1o  8093  frxp  8108  xporderlem  8109  poxp  8110  fnwelem  8113  poxp2  8125  xpord3pred  8134  poseq  8140  soseq  8141  suppimacnv  8156  rexsupp  8164  mpocurryd  8251  smoel2  8335  omeu  8552  oeeui  8569  omabs  8618  omopth  8629  eldifsucnn  8631  qliftel  8776  brecop  8786  eroveu  8788  erov  8790  ecopovtrn  8796  ixpsnf1o  8914  dom2lem  8966  mapsnend  9010  xpsnen  9029  xpassen  9040  pw2f1olem  9050  xpf1o  9109  unxpdom  9207  domunfican  9279  preleqALT  9577  zfinf  9599  cantnfs  9626  brttrcl  9673  ttrclselem2  9686  tcvalg  9698  r0weon  9972  fseqenlem1  9984  acni2  10006  aceq1  10077  aceq0  10078  dfac5lem4  10086  dfac2a  10090  dfac12lem2  10105  cardcf  10212  cfeq0  10216  cfsuc  10217  cff1  10218  cfss  10225  isf32lem5  10317  fin1a2lem6  10365  zfac  10420  brdom7disj  10491  brdom6disj  10492  axrepnd  10554  axunndlem1  10555  axinfnd  10566  axacndlem5  10571  axacnd  10572  zfcndrep  10574  zfcndinf  10578  zfcndac  10579  pwfseqlem4a  10621  pwfseqlem4  10622  gruina  10778  grothomex  10789  ordpipq  10902  elnpi  10948  genpass  10969  ltprord  10990  reclem2pr  11008  reclem3pr  11009  recexpr  11011  addsrmo  11033  mulsrmo  11034  addsrpr  11035  mulsrpr  11036  ltsosr  11054  mulgt0sr  11065  supsr  11072  ltresr  11100  axpre-lttrn  11126  axpre-mulgt0  11128  prime  12622  peano5uzti  12631  rexuz  12864  ltxr  13082  qbtwnre  13166  xmulneg1  13236  supxr2  13281  ixxval  13321  fzval  13477  preduz  13618  nn0opth2  14244  hashbclem  14424  hashf1lem2  14428  eqwrd  14529  pfxeq  14668  wrd2ind  14695  cshwcsh2id  14801  eqwrds3  14934  cleq1lem  14955  rtrclreclem3  15033  rtrclreclem4  15034  relexpindlem  15036  abslt  15288  absle  15289  lenegsq  15294  abs2difabs  15308  ello12  15489  elo12  15500  o1lo1  15510  rlimuni  15523  lo1resb  15537  o1resb  15539  2clim  15545  rlimcn3  15563  climcn2  15566  addcn2  15567  mulcn2  15569  o1of2  15586  sumeq1  15662  fsum2dlem  15743  modfsummod  15767  prodeq1f  15879  prodeq1  15880  fprod2dlem  15953  nndivdvds  16238  divalg2  16382  smupval  16465  gcdval  16473  gcdass  16524  lcmval  16569  lcmass  16591  rpexp  16699  pythagtriplem2  16795  pythagtrip  16812  vdwapun  16952  0ram  16998  ramub1lem2  17005  pwsle  17462  imasleval  17511  ismre  17558  ismri  17599  iscatd2  17649  dfiso2  17741  isssc  17789  funcpropd  17871  fullpropd  17891  fthres2b  17901  fthres2c  17902  setcsect  18058  cat1lem  18065  cat1  18066  prslem  18265  drsdir  18270  posi  18285  tosso  18385  odudlatb  18491  ipoval  18496  ipolt  18501  dirge  18569  gsumpropd2lem  18613  mgmhmpropd  18632  issgrpv  18655  issgrpn0  18656  ismhm0  18724  mhmpropd  18726  mndind  18762  mgmnsgrpex  18865  issubg3  19083  isga  19230  symgfixelq  19370  psgnfval  19437  psgnval  19444  dprdw  19949  subgdmdprd  19973  isrnghm  20357  issubrg  20487  resrhm2b  20518  rngcsect  20552  rngcinv  20553  ringcsect  20586  ringcinv  20587  drngpropd  20685  islmod  20777  lmodlema  20778  lmodprop2d  20837  lsslss  20874  lbspropd  21013  lbsacsbs  21073  znleval  21471  islbs4  21748  islinds3  21750  aspval2  21814  psrbag  21833  pf1ind  22249  mdetunilem4  22509  mdetunilem9  22514  istopg  22789  basis2  22845  tg2  22859  iscld  22921  isnei  22997  isneip  22999  neiptoptop  23025  neiptopnei  23026  neitr  23074  restlp  23077  iscn  23129  cnpval  23130  iscnp  23131  regsep  23228  1stcclb  23338  2ndc1stc  23345  2ndcctbss  23349  2ndcdisj  23350  llyi  23368  nllyi  23369  hausmapdom  23394  locfinnei  23417  comppfsc  23426  elkgen  23430  txbas  23461  txcls  23498  txcnpi  23502  ptpjopn  23506  txdis1cn  23529  txtube  23534  txcmplem1  23535  hausdiag  23539  tx1stc  23544  txkgen  23546  xkococn  23554  elqtop  23591  kqreglem1  23635  elmptrab  23721  isfbas  23723  elflim2  23858  elflim  23865  hauspwpwf1  23881  alexsublem  23938  ghmcnp  24009  qustgplem  24015  tsmssubm  24037  elutop  24128  ustuqtop4  24139  isucn  24172  iscfilu  24182  ispsmet  24199  ismet  24218  isxmet  24219  ismet2  24228  imasdsf1olem  24268  blres  24326  elmopn  24337  mopni  24387  neibl  24396  nrmmetd  24469  ngppropd  24532  elcncf  24789  mulc1cncf  24805  elpi1  24952  isclmp  25004  metcld2  25214  pmltpclem1  25356  itg1climres  25622  itg2val  25636  isibl  25673  itgeq1f  25679  itgeq1fOLD  25680  itgeq1  25681  cbvitgv  25685  itgresr  25687  iblcn  25707  itgfsum  25735  dvreslem  25817  dvfsumlem2  25940  dvfsumlem2OLD  25941  deg1ldg  26004  vieta1  26227  ulm2  26301  sincosq2sgn  26415  sincosq4sgn  26417  efopn  26574  dvdsflsumcom  27105  fsumvma2  27132  logfac2  27135  dchrptlem1  27182  lgsdchrval  27272  2lgslem1a  27309  pntibndlem3  27510  pntlemi  27522  pntleme  27526  pnt3  27530  sltval  27566  nolt02o  27614  slelttr  27676  nocvxminlem  27696  madebday  27818  sltlpss  27826  addsprop  27890  mulsproplemcbv  28025  mulsproplem1  28026  mulsprop  28040  absslt  28158  eucliddivs  28272  zs12ge0  28349  istrkgld  28393  istrkg2ld  28394  istrkg3ld  28395  axtgsegcon  28398  axtg5seg  28399  axtgpasch  28401  axtgupdim2  28405  legov  28519  islnopp  28673  ishpg  28693  iscgra1  28744  dfcgra2  28764  dfcgrg2  28797  brcgr  28834  brbtwn2  28839  axsegconlem1  28851  axsegcon  28861  axcontlem10  28907  edgssv2  29132  uhgr2edg  29142  isfusgrf1  29254  edgnbusgreu  29301  cplgr3v  29369  vtxdun  29416  upgr2wlk  29603  upgrtrls  29636  upgristrl  29637  upgrf1istrl  29638  dfpth2  29666  2pthnloop  29668  usgr2pth  29701  isclwlke  29714  isclwlkupgr  29715  iswwlksnx  29777  wlknewwlksn  29824  2pthon3v  29880  elwwlks2on  29896  wpthswwlks2on  29898  rusgrnumwwlkl1  29905  rusgrnumwwlkb0  29908  clwwlknp  29973  clwwlkf  29983  erclwwlknsym  30006  erclwwlkntr  30007  clwwlknonwwlknonb  30042  0trl  30058  0spth  30062  0crct  30069  0cycl  30070  upgr4cycl4dv4e  30121  upgriseupth  30143  eupth2lem2  30155  3cyclfrgrrn1  30221  4cycl2vnunb  30226  frgrncvvdeqlem2  30236  frgr2wwlk1  30265  fusgr2wsp2nb  30270  numclwlk1lem1  30305  vciOLD  30497  isvclem  30513  nmoofval  30698  isph  30758  norm3lemt  31088  isch2  31159  cmbr  31520  eigre  31771  eigorth  31774  nmopub  31844  nmfnleub  31861  cvbr  32218  mdbr  32230  dmdbr  32235  chrelat2  32306  mdsymlem2  32340  rexunirn  32428  ifeqeqx  32478  iunrnmptss  32501  funcnvmpt  32598  fdifsupp  32615  ressupprn  32620  1stpreima  32637  fpwrelmapffslem  32662  isomnd  33022  archirng  33149  isslmd  33162  slmdlema  33163  urpropd  33190  orngmul  33288  lindflbs  33357  islbs5  33358  lindfpropd  33360  opprqus0g  33468  idlsrgval  33481  ressply1mon1p  33544  ccfldextdgrr  33674  constrsslem  33738  constrconj  33742  constrlccllem  33750  constrcbvlem  33752  dya2iocuni  34281  omsfval  34292  elcarsg  34303  itgeq12dv  34324  isrrvv  34441  reprinrn  34616  reprdifc  34625  istrkg2d  34664  axtgupdim2ALTV  34666  brafs  34670  bnj956  34773  bnj1146  34788  bnj18eq1  34924  axsepg2  35079  axsepg2ALT  35080  zltp1ne  35104  isacycgr  35139  kur14  35210  pconncn  35218  cnpconn  35224  txpconn  35226  cvmscbv  35252  cvmcov  35257  cvmsi  35259  cvmsval  35260  cvmopnlem  35272  cvmlift2lem10  35306  cvmlift3lem2  35314  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  cvmlift3  35322  satf0op  35371  sat1el2xp  35373  satffunlem  35395  dmopab3rexdif  35399  mclsssvlem  35556  mclsind  35564  rexxfr3dALT  35633  eldm3  35755  opelco3  35769  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  dfon2  35787  elfuns  35910  brsuccf  35936  brofs  36000  5segofs  36001  brifs  36038  ifscgr  36039  brcolinear  36054  lineext  36071  brfs  36074  fscgr  36075  linecgr  36076  btwnconn1lem4  36085  btwnconn1lem8  36089  btwnconn1lem11  36092  btwnconn1lem12  36093  segcon2  36100  brsegle  36103  outsideofeq  36125  funray  36135  funline  36137  fvline  36139  linethru  36148  disjeq12dv  36210  prodeq12sdv  36213  itgeq12sdv  36214  cbvitgvw2  36243  cbvitgdavw  36276  cbvitgdavw2  36292  trer  36311  finminlem  36313  ivthALT  36330  filnetlem4  36376  knoppndvlem21  36527  bj-zfauscl  36919  bj-elgab  36934  bj-imdirvallem  37175  csboprabg  37325  topdifinffinlem  37342  icoreval  37348  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  pibp19  37409  wl-ax11-lem8  37587  curf  37599  ptrest  37620  poimirlem1  37622  poimirlem13  37634  poimirlem14  37635  poimirlem22  37643  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  heicant  37656  mblfinlem3  37660  mblfinlem4  37661  mbfresfi  37667  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  areacirclem5  37713  cover2  37716  cover2g  37717  fdc  37746  fdc1  37747  heibor1  37811  bfp  37825  rngosn3  37925  drngoi  37952  isdrngo1  37957  isriscg  37985  isfldidl2  38070  eldmxrncnvepres  38403  brressn  38439  islshpat  39017  lcvbr  39021  lshpsmreu  39109  ldual1dim  39166  cvrval  39269  cvrnbtwn3  39276  iscvlat2N  39324  ishlat3N  39354  hlrelat5N  39402  3dim0  39458  llnexatN  39522  islpln5  39536  islvol5  39580  pmapjat1  39854  ltrnu  40122  cdleme02N  40223  cdlemg33b  40708  cdlemg33c  40709  dvhb1dimN  40987  dibelval3  41148  dibopelval3  41149  dib1dim  41166  dibglbN  41167  diblsmopel  41172  dicval  41177  dicopelval  41178  dicelval3  41181  dicelval1sta  41188  dihopelvalcpre  41249  dih1dimatlem  41330  dihpN  41337  dihjatcclem4  41422  lpolsetN  41483  mapdpglem3  41676  hdmapglem7a  41928  sticksstones23  42164  exfinfldd  42198  fimgmcyclem  42528  fimgmcyc  42529  fsuppind  42585  fsuppssindlem2  42587  prjspeclsp  42607  mrefg2  42702  mzpclval  42720  eldiophb  42752  eldioph2lem1  42755  eldioph3  42761  lzenom  42765  diophin  42767  eldiophss  42769  diophrex  42770  eq0rabdioph  42771  pellexlem3  42826  elpell1qr  42842  elpell14qr  42844  elpell1234qr  42846  jm2.27  43004  rmydioph  43010  expdiophlem1  43017  expdioph  43019  pw2f1ocnv  43033  hbtlem1  43119  hbtlem7  43121  dgraalem  43141  dgraaub  43144  dflim7  43269  omabs2  43328  tfsconcatfv2  43336  tfsconcat0i  43341  nadd1suc  43388  ifpbi2  43463  inintabd  43575  cnvcnvintabd  43596  cnvintabd  43599  clcnvlem  43619  iunrelexpmin1  43704  uneqsn  44021  k0004lem2  44144  mnuprdlem1  44268  mnuprdlem2  44269  binomcxplemnotnn0  44352  2sbc6g  44411  2sbc5g  44412  iotasbc  44415  dropab1  44443  dropab2  44444  relpeq5  44945  modelaxreplem3  44977  omssaxinf2  44985  brpermmodel  45000  permaxinf2lem  45009  cbvmpo1  45099  r19.28zf  45160  disjinfi  45193  dmrelrnrel  45227  mullimc  45621  mullimcf  45628  limsuppnfd  45707  limsuppnf  45716  limsupre2  45730  limsupre2mpt  45735  limsupre3  45738  limsupre3mpt  45739  limsupre3uzlem  45740  fourierdlem42  46154  fourierdlem48  46159  fourierdlem50  46161  fourierdlem51  46162  fourierdlem54  46165  fourierdlem86  46197  ovnval2  46550  ovnsubaddlem1  46575  hoiqssbl  46630  vonicclem2  46689  f1cof1b  47082  f1ocof1ob2  47087  funressnbrafv2  47249  dfatdmfcoafv2  47259  2ffzoeq  47332  fundcmpsurbijinj  47415  ichreuopeq  47478  prproropf1olem4  47511  prprspr2  47523  prprsprreu  47524  prprreueq  47525  reuopreuprim  47531  isubgrgrim  47933  grtriprop  47944  isgrtri  47946  opgpgvtx  48050  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113  rngcsectALTV  48267  rngcinvALTV  48268  ringcsectALTV  48301  ringcinvALTV  48302  lmod1  48485  elbigo2  48545  rrx2vlinest  48734  eloprab1st2nd  48860  i0oii  48912  io1ii  48913  lubeldm2d  48950  glbeldm2d  48951  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  uppropd  49174  functhinc  49441  fullthinc  49443