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  1609  drsb1  2495  eleq1w  2814  eleq1d  2816  clelab  2876  rexeqfOLD  3323  rmoeq1OLD  3379  reueq1OLD  3380  rmoeq1f  3385  rabeq  3409  rabeqbidva  3411  rabeqd  3423  rabeqf  3429  cgsex4gOLD  3484  vtocl2gafOLD  3531  vtocl4gaOLD  3538  alexeqg  3601  reu2eqd  3690  sbc2or  3745  sbc5ALT  3765  rexssOLD  4007  psstr  4052  difin2  4246  r19.28z  4443  dfif6  4473  rabsneq  4590  rexreusng  4627  reurexprg  4652  rabsnifsb  4670  ssunsn2  4774  preq12bg  4800  opeq1  4820  eluni  4857  csbuni  4883  unissb  4886  iuneq12d  4966  disjxun  5084  unopab  5166  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  dftr2c  5196  axrep1  5213  axreplem  5214  zfrepclf  5224  axsepgfromrep  5227  axsepg  5230  zfauscl  5231  reusv2lem4  5334  rabxfrd  5350  opthg  5412  otthg  5420  copsexgw  5425  copsexg  5426  opeqsng  5438  euotd  5448  elopabw  5461  pocl  5527  xpeq1  5625  elxpi  5633  vtoclr  5674  opbrop  5709  dmopab2rex  5852  resopab2  5980  rnco  6194  dflim2  6359  dffun2  6486  fun11  6550  feq2  6625  f1eq2  6710  f1eq3  6711  foeq2  6727  brprcneu  6807  brprcneuALT  6808  ssimaexg  6903  dmfco  6913  fndmdif  6970  respreima  6994  isoeq5  7250  isoini  7267  isopolem  7274  f1oiso  7280  f1oiso2  7281  imaeqsexvOLD  7292  riotaeqdv  7299  oprabidw  7372  oprabid  7373  oprabv  7401  mpoeq123  7413  mpoeq123dva  7415  0mpo0  7424  eloprabga  7450  resoprab  7459  resoprab2  7460  elrnmpores  7479  ov  7485  ov3  7504  ov6g  7505  ovg  7506  imaeqexov  7579  caoftrn  7646  uniuni  7690  limuni3  7777  elxp4  7847  elxp5  7848  opabex3d  7892  opabex3rd  7893  opabex3  7894  releldmdifi  7972  opiota  7986  eloprabi  7990  mptmpoopabbrd  8007  mptmpoopabbrdOLD  8008  cnvf1o  8036  frxp  8051  xporderlem  8052  poxp  8053  fnwelem  8056  poxp2  8068  xpord3pred  8077  poseq  8083  soseq  8084  suppimacnv  8099  rexsupp  8107  mpocurryd  8194  smoel2  8278  omeu  8495  oeeui  8512  omabs  8561  omopth  8572  eldifsucnn  8574  qliftel  8719  brecop  8729  eroveu  8731  erov  8733  ecopovtrn  8739  ixpsnf1o  8857  dom2lem  8909  mapsnend  8953  xpsnen  8969  xpassen  8979  pw2f1olem  8989  xpf1o  9047  unxpdom  9138  domunfican  9201  preleqALT  9502  zfinf  9524  cantnfs  9551  brttrcl  9598  ttrclselem2  9611  tcvalg  9621  r0weon  9898  fseqenlem1  9910  acni2  9932  aceq1  10003  aceq0  10004  dfac5lem4  10012  dfac2a  10016  dfac12lem2  10031  cardcf  10138  cfeq0  10142  cfsuc  10143  cff1  10144  cfss  10151  isf32lem5  10243  fin1a2lem6  10291  zfac  10346  brdom7disj  10417  brdom6disj  10418  axrepnd  10480  axunndlem1  10481  axinfnd  10492  axacndlem5  10497  axacnd  10498  zfcndrep  10500  zfcndinf  10504  zfcndac  10505  pwfseqlem4a  10547  pwfseqlem4  10548  gruina  10704  grothomex  10715  ordpipq  10828  elnpi  10874  genpass  10895  ltprord  10916  reclem2pr  10934  reclem3pr  10935  recexpr  10937  addsrmo  10959  mulsrmo  10960  addsrpr  10961  mulsrpr  10962  ltsosr  10980  mulgt0sr  10991  supsr  10998  ltresr  11026  axpre-lttrn  11052  axpre-mulgt0  11054  prime  12549  peano5uzti  12558  rexuz  12791  ltxr  13009  qbtwnre  13093  xmulneg1  13163  supxr2  13208  ixxval  13248  fzval  13404  preduz  13545  nn0opth2  14174  hashbclem  14354  hashf1lem2  14358  eqwrd  14459  pfxeq  14598  wrd2ind  14625  cshwcsh2id  14730  eqwrds3  14863  cleq1lem  14884  rtrclreclem3  14962  rtrclreclem4  14963  relexpindlem  14965  abslt  15217  absle  15218  lenegsq  15223  abs2difabs  15237  ello12  15418  elo12  15429  o1lo1  15439  rlimuni  15452  lo1resb  15466  o1resb  15468  2clim  15474  rlimcn3  15492  climcn2  15495  addcn2  15496  mulcn2  15498  o1of2  15515  sumeq1  15591  fsum2dlem  15672  modfsummod  15696  prodeq1f  15808  prodeq1  15809  fprod2dlem  15882  nndivdvds  16167  divalg2  16311  smupval  16394  gcdval  16402  gcdass  16453  lcmval  16498  lcmass  16520  rpexp  16628  pythagtriplem2  16724  pythagtrip  16741  vdwapun  16881  0ram  16927  ramub1lem2  16934  pwsle  17391  imasleval  17440  ismre  17487  ismri  17532  iscatd2  17582  dfiso2  17674  isssc  17722  funcpropd  17804  fullpropd  17824  fthres2b  17834  fthres2c  17835  setcsect  17991  cat1lem  17998  cat1  17999  prslem  18198  drsdir  18203  posi  18218  tosso  18318  odudlatb  18426  ipoval  18431  ipolt  18436  dirge  18504  gsumpropd2lem  18582  mgmhmpropd  18601  issgrpv  18624  issgrpn0  18625  ismhm0  18693  mhmpropd  18695  mndind  18731  mgmnsgrpex  18834  issubg3  19052  isga  19198  symgfixelq  19340  psgnfval  19407  psgnval  19414  dprdw  19919  subgdmdprd  19943  isomnd  20030  isrnghm  20354  issubrg  20481  resrhm2b  20512  rngcsect  20546  rngcinv  20547  ringcsect  20580  ringcinv  20581  drngpropd  20679  orngmul  20775  islmod  20792  lmodlema  20793  lmodprop2d  20852  lsslss  20889  lbspropd  21028  lbsacsbs  21088  znleval  21486  islbs4  21764  islinds3  21766  aspval2  21830  psrbag  21849  pf1ind  22265  mdetunilem4  22525  mdetunilem9  22530  istopg  22805  basis2  22861  tg2  22875  iscld  22937  isnei  23013  isneip  23015  neiptoptop  23041  neiptopnei  23042  neitr  23090  restlp  23093  iscn  23145  cnpval  23146  iscnp  23147  regsep  23244  1stcclb  23354  2ndc1stc  23361  2ndcctbss  23365  2ndcdisj  23366  llyi  23384  nllyi  23385  hausmapdom  23410  locfinnei  23433  comppfsc  23442  elkgen  23446  txbas  23477  txcls  23514  txcnpi  23518  ptpjopn  23522  txdis1cn  23545  txtube  23550  txcmplem1  23551  hausdiag  23555  tx1stc  23560  txkgen  23562  xkococn  23570  elqtop  23607  kqreglem1  23651  elmptrab  23737  isfbas  23739  elflim2  23874  elflim  23881  hauspwpwf1  23897  alexsublem  23954  ghmcnp  24025  qustgplem  24031  tsmssubm  24053  elutop  24143  ustuqtop4  24154  isucn  24187  iscfilu  24197  ispsmet  24214  ismet  24233  isxmet  24234  ismet2  24243  imasdsf1olem  24283  blres  24341  elmopn  24352  mopni  24402  neibl  24411  nrmmetd  24484  ngppropd  24547  elcncf  24804  mulc1cncf  24820  elpi1  24967  isclmp  25019  metcld2  25229  pmltpclem1  25371  itg1climres  25637  itg2val  25651  isibl  25688  itgeq1f  25694  itgeq1fOLD  25695  itgeq1  25696  cbvitgv  25700  itgresr  25702  iblcn  25722  itgfsum  25750  dvreslem  25832  dvfsumlem2  25955  dvfsumlem2OLD  25956  deg1ldg  26019  vieta1  26242  ulm2  26316  sincosq2sgn  26430  sincosq4sgn  26432  efopn  26589  dvdsflsumcom  27120  fsumvma2  27147  logfac2  27150  dchrptlem1  27197  lgsdchrval  27287  2lgslem1a  27324  pntibndlem3  27525  pntlemi  27537  pntleme  27541  pnt3  27545  sltval  27581  nolt02o  27629  slelttr  27691  nocvxminlem  27712  madebday  27840  sltlpss  27848  addsprop  27914  mulsproplemcbv  28049  mulsproplem1  28050  mulsprop  28064  absslt  28182  eucliddivs  28296  zs12ge0  28388  istrkgld  28432  istrkg2ld  28433  istrkg3ld  28434  axtgsegcon  28437  axtg5seg  28438  axtgpasch  28440  axtgupdim2  28444  legov  28558  islnopp  28712  ishpg  28732  iscgra1  28783  dfcgra2  28803  dfcgrg2  28836  brcgr  28873  brbtwn2  28878  axsegconlem1  28890  axsegcon  28900  axcontlem10  28946  edgssv2  29171  uhgr2edg  29181  isfusgrf1  29293  edgnbusgreu  29340  cplgr3v  29408  vtxdun  29455  upgr2wlk  29640  upgrtrls  29673  upgristrl  29674  upgrf1istrl  29675  dfpth2  29702  2pthnloop  29704  usgr2pth  29737  isclwlke  29750  isclwlkupgr  29751  iswwlksnx  29813  wlknewwlksn  29860  2pthon3v  29916  elwwlks2on  29932  wpthswwlks2on  29934  rusgrnumwwlkl1  29941  rusgrnumwwlkb0  29944  clwwlknp  30009  clwwlkf  30019  erclwwlknsym  30042  erclwwlkntr  30043  clwwlknonwwlknonb  30078  0trl  30094  0spth  30098  0crct  30105  0cycl  30106  upgr4cycl4dv4e  30157  upgriseupth  30179  eupth2lem2  30191  3cyclfrgrrn1  30257  4cycl2vnunb  30262  frgrncvvdeqlem2  30272  frgr2wwlk1  30301  fusgr2wsp2nb  30306  numclwlk1lem1  30341  vciOLD  30533  isvclem  30549  nmoofval  30734  isph  30794  norm3lemt  31124  isch2  31195  cmbr  31556  eigre  31807  eigorth  31810  nmopub  31880  nmfnleub  31897  cvbr  32254  mdbr  32266  dmdbr  32271  chrelat2  32342  mdsymlem2  32376  rexunirn  32463  ifeqeqx  32514  iunrnmptss  32537  funcnvmpt  32641  fdifsupp  32658  ressupprn  32663  1stpreima  32680  fpwrelmapffslem  32707  archirng  33149  isslmd  33163  slmdlema  33164  urpropd  33191  lindflbs  33336  islbs5  33337  lindfpropd  33339  opprqus0g  33447  idlsrgval  33460  ressply1mon1p  33523  ccfldextdgrr  33677  constrsslem  33746  constrconj  33750  constrlccllem  33758  constrcbvlem  33760  dya2iocuni  34288  omsfval  34299  elcarsg  34310  itgeq12dv  34331  isrrvv  34448  reprinrn  34623  reprdifc  34632  istrkg2d  34671  axtgupdim2ALTV  34673  brafs  34677  bnj956  34780  bnj1146  34795  bnj18eq1  34931  axsepg2  35086  axsepg2ALT  35087  zltp1ne  35146  isacycgr  35181  kur14  35252  pconncn  35260  cnpconn  35266  txpconn  35268  cvmscbv  35294  cvmcov  35299  cvmsi  35301  cvmsval  35302  cvmopnlem  35314  cvmlift2lem10  35348  cvmlift3lem2  35356  cvmlift3lem6  35360  cvmlift3lem7  35361  cvmlift3lem9  35363  cvmlift3  35364  satf0op  35413  sat1el2xp  35415  satffunlem  35437  dmopab3rexdif  35441  mclsssvlem  35598  mclsind  35606  rexxfr3dALT  35675  eldm3  35797  opelco3  35811  dfon2lem6  35822  dfon2lem7  35823  dfon2lem8  35824  dfon2  35826  elfuns  35949  brsuccf  35975  brofs  36039  5segofs  36040  brifs  36077  ifscgr  36078  brcolinear  36093  lineext  36110  brfs  36113  fscgr  36114  linecgr  36115  btwnconn1lem4  36124  btwnconn1lem8  36128  btwnconn1lem11  36131  btwnconn1lem12  36132  segcon2  36139  brsegle  36142  outsideofeq  36164  funray  36174  funline  36176  fvline  36178  linethru  36187  disjeq12dv  36249  prodeq12sdv  36252  itgeq12sdv  36253  cbvitgvw2  36282  cbvitgdavw  36315  cbvitgdavw2  36331  trer  36350  finminlem  36352  ivthALT  36369  filnetlem4  36415  knoppndvlem21  36566  bj-zfauscl  36958  bj-elgab  36973  bj-imdirvallem  37214  csboprabg  37364  topdifinffinlem  37381  icoreval  37387  isbasisrelowllem1  37389  isbasisrelowllem2  37390  relowlssretop  37397  pibp19  37448  wl-ax11-lem8  37626  curf  37638  ptrest  37659  poimirlem1  37661  poimirlem13  37673  poimirlem14  37674  poimirlem22  37682  poimirlem24  37684  poimirlem26  37686  poimirlem27  37687  heicant  37695  mblfinlem3  37699  mblfinlem4  37700  mbfresfi  37706  itg2addnclem3  37713  itg2addnc  37714  itg2gt0cn  37715  areacirclem5  37752  cover2  37755  cover2g  37756  fdc  37785  fdc1  37786  heibor1  37850  bfp  37864  rngosn3  37964  drngoi  37991  isdrngo1  37996  isriscg  38024  isfldidl2  38109  eldmxrncnvepres  38442  brressn  38478  islshpat  39056  lcvbr  39060  lshpsmreu  39148  ldual1dim  39205  cvrval  39308  cvrnbtwn3  39315  iscvlat2N  39363  ishlat3N  39393  hlrelat5N  39440  3dim0  39496  llnexatN  39560  islpln5  39574  islvol5  39618  pmapjat1  39892  ltrnu  40160  cdleme02N  40261  cdlemg33b  40746  cdlemg33c  40747  dvhb1dimN  41025  dibelval3  41186  dibopelval3  41187  dib1dim  41204  dibglbN  41205  diblsmopel  41210  dicval  41215  dicopelval  41216  dicelval3  41219  dicelval1sta  41226  dihopelvalcpre  41287  dih1dimatlem  41368  dihpN  41375  dihjatcclem4  41460  lpolsetN  41521  mapdpglem3  41714  hdmapglem7a  41966  sticksstones23  42202  exfinfldd  42236  fimgmcyclem  42566  fimgmcyc  42567  fsuppind  42623  fsuppssindlem2  42625  prjspeclsp  42645  mrefg2  42740  mzpclval  42758  eldiophb  42790  eldioph2lem1  42793  eldioph3  42799  lzenom  42803  diophin  42805  eldiophss  42807  diophrex  42808  eq0rabdioph  42809  pellexlem3  42864  elpell1qr  42880  elpell14qr  42882  elpell1234qr  42884  jm2.27  43041  rmydioph  43047  expdiophlem1  43054  expdioph  43056  pw2f1ocnv  43070  hbtlem1  43156  hbtlem7  43158  dgraalem  43178  dgraaub  43181  dflim7  43306  omabs2  43365  tfsconcatfv2  43373  tfsconcat0i  43378  nadd1suc  43425  ifpbi2  43500  inintabd  43612  cnvcnvintabd  43633  cnvintabd  43636  clcnvlem  43656  iunrelexpmin1  43741  uneqsn  44058  k0004lem2  44181  mnuprdlem1  44305  mnuprdlem2  44306  binomcxplemnotnn0  44389  2sbc6g  44448  2sbc5g  44449  iotasbc  44452  dropab1  44479  dropab2  44480  relpeq5  44981  modelaxreplem3  45013  omssaxinf2  45021  brpermmodel  45036  permaxinf2lem  45045  cbvmpo1  45135  r19.28zf  45196  disjinfi  45229  dmrelrnrel  45263  mullimc  45656  mullimcf  45663  limsuppnfd  45740  limsuppnf  45749  limsupre2  45763  limsupre2mpt  45768  limsupre3  45771  limsupre3mpt  45772  limsupre3uzlem  45773  fourierdlem42  46187  fourierdlem48  46192  fourierdlem50  46194  fourierdlem51  46195  fourierdlem54  46198  fourierdlem86  46230  ovnval2  46583  ovnsubaddlem1  46608  hoiqssbl  46663  vonicclem2  46722  f1cof1b  47108  f1ocof1ob2  47113  funressnbrafv2  47275  dfatdmfcoafv2  47285  2ffzoeq  47358  fundcmpsurbijinj  47441  ichreuopeq  47504  prproropf1olem4  47537  prprspr2  47549  prprsprreu  47550  prprreueq  47551  reuopreuprim  47557  isubgrgrim  47960  grtriprop  47972  isgrtri  47974  opgpgvtx  48086  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem4  48150  grlimedgnedg  48162  rngcsectALTV  48306  rngcinvALTV  48307  ringcsectALTV  48340  ringcinvALTV  48341  lmod1  48524  elbigo2  48584  rrx2vlinest  48773  eloprab1st2nd  48899  i0oii  48951  io1ii  48952  lubeldm2d  48989  glbeldm2d  48990  sectpropdlem  49068  invpropdlem  49070  isopropdlem  49072  uppropd  49213  functhinc  49480  fullthinc  49482