Theorem anbi1d 737

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
bid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 670	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anbi1  739  anbi12d  743  bi2anan9  913  pm5.71  973  cador  1538  drsb1  2365  eleq1d  2672  rexeqf  3112  reueq1f  3113  rmoeq1f  3114  rabeqf  3165  vtocl2gaf  3246  vtocl4ga  3251  alexeqg  3302  elrabi  3328  reu2eqd  3370  sbc2or  3411  sbc5  3427  rexss  3632  psstr  3673  ineq1  3769  difin2  3849  r19.28z  4015  rabsnifsb  4201  ssunsn2  4299  preq12bg  4326  prel12g  4327  opeq1  4340  eluni  4375  csbuni  4402  disjxun  4581  mpteq12f  4661  axrep1  4700  axrep2  4701  axrep3  4702  zfrepclf  4705  axsep  4708  axsep2  4710  zfauscl  4711  reusv2lem4  4798  rabxfrd  4815  opthg  4872  otthg  4880  copsexg  4882  euotd  4900  elopab  4908  pocl  4966  xpeq1  5052  elxpi  5054  vtoclr  5086  opbrop  5121  opelresg  5324  resopab2  5368  dflim2  5698  fun11  5877  feq2  5940  f1eq2  6010  f1eq3  6011  foeq2  6025  brprcneu  6096  ssimaexg  6174  dmfco  6182  fndmdif  6229  respreima  6252  isoeq5  6471  isoini  6488  isopolem  6495  f1oiso  6501  f1oiso2  6502  riotaeqdv  6512  oprabid  6576  oprabv  6601  mpt2eq123  6612  mpt2eq123dva  6614  eloprabga  6645  resoprab  6654  resoprab2  6655  elrnmpt2res  6672  ov  6678  ov3  6695  ov6g  6696  ovg  6697  caoftrn  6830  uniuni  6865  limuni3  6944  elxp4  7003  elxp5  7004  opabex3d  7037  opabex3  7038  opiota  7118  eloprabi  7121  cnvf1o  7163  frxp  7174  xporderlem  7175  poxp  7176  fnwelem  7179  suppimacnv  7193  rexsupp  7200  mpt2curryd  7282  smoel2  7347  omeu  7552  oeeui  7569  omabs  7614  omopth  7625  qliftel  7717  brecop  7727  eroveu  7729  erov  7731  ecopovtrn  7737  ixpsnf1o  7834  dom2lem  7881  xpsnen  7929  xpassen  7939  pw2f1olem  7949  xpf1o  8007  unxpdom  8052  domunfican  8118  preleq  8397  zfinf  8419  cantnfs  8446  tcvalg  8497  r0weon  8718  fseqenlem1  8730  acni2  8752  aceq1  8823  aceq0  8824  dfac2a  8835  dfac12lem2  8849  cardcf  8957  cfeq0  8961  cfsuc  8962  cff1  8963  cfss  8970  isf32lem5  9062  fin1a2lem6  9110  zfac  9165  brdom7disj  9234  brdom6disj  9235  axrepnd  9295  axunndlem1  9296  axinfnd  9307  axacndlem5  9312  axacnd  9313  zfcndrep  9315  zfcndinf  9319  zfcndac  9320  pwfseqlem4a  9362  pwfseqlem4  9363  gruina  9519  grothomex  9530  ordpipq  9643  elnpi  9689  genpass  9710  ltprord  9731  reclem2pr  9749  reclem3pr  9750  recexpr  9752  addsrmo  9773  mulsrmo  9774  addsrpr  9775  mulsrpr  9776  ltsosr  9794  mulgt0sr  9805  supsr  9812  ltresr  9840  axpre-lttrn  9866  axpre-mulgt0  9868  prime  11334  peano5uzti  11343  rexuz  11614  ltxr  11825  qbtwnre  11904  xmulneg1  11971  supxr2  12016  ixxval  12054  fzval  12199  preduz  12330  nn0opth2  12921  hashbclem  13093  hashf1lem2  13097  eqwrd  13201  swrdeq  13296  wrd2ind  13329  cshwcsh2id  13425  eqwrds3  13552  cleq1lem  13569  rtrclreclem3  13648  rtrclreclem4  13649  relexpindlem  13651  abslt  13902  absle  13903  lenegsq  13908  abs2difabs  13922  ello12  14095  elo12  14106  o1lo1  14116  rlimuni  14129  lo1resb  14143  o1resb  14145  2clim  14151  rlimcn2  14169  climcn2  14171  addcn2  14172  mulcn2  14174  o1of2  14191  sumeq1  14267  fsum2dlem  14343  modfsummod  14367  prodeq1f  14477  fprod2dlem  14549  znnenlem  14779  nndivdvds  14827  zeneo  14901  divalg2  14966  smupval  15048  gcdval  15056  gcdass  15102  lcmval  15143  lcmass  15165  rpexp  15270  pythagtriplem2  15360  pythagtrip  15377  vdwapun  15516  0ram  15562  ramub1lem2  15569  pwsle  15975  imasleval  16024  ismre  16073  ismri  16114  iscatd2  16165  dfiso2  16255  isssc  16303  funcpropd  16383  fullpropd  16403  fthres2b  16413  fthres2c  16414  setcsect  16562  prslem  16754  drsdir  16758  posi  16773  tosso  16859  ipoval  16977  ipolt  16982  odudlatb  17019  dirge  17060  gsumpropd2lem  17096  issgrpv  17109  issgrpn0  17110  mhmpropd  17164  mrcmndind  17189  mgmnsgrpex  17241  issubg3  17435  isga  17547  symgfixelq  17676  psgnfval  17743  psgnval  17750  isslw  17846  dprdw  18232  subgdmdprd  18256  drngpropd  18597  issubrg  18603  islmod  18690  lmodlema  18691  lmodprop2d  18748  lsslss  18782  lbspropd  18920  lbsacsbs  18977  aspval2  19168  psrbag  19185  pf1ind  19540  znleval  19722  islbs4  19990  islinds3  19992  mdetunilem4  20240  mdetunilem9  20245  istopg  20525  basis2  20566  tg2  20580  iscld  20641  neival  20716  isnei  20717  isneip  20719  neiptoptop  20745  neiptopnei  20746  neitr  20794  restlp  20797  iscn  20849  cnpval  20850  iscnp  20851  regsep  20948  nrmsep3  20969  1stcclb  21057  2ndc1stc  21064  2ndcctbss  21068  2ndcdisj  21069  llyi  21087  nllyi  21088  hausmapdom  21113  locfinnei  21136  comppfsc  21145  elkgen  21149  txbas  21180  txcls  21217  txcnpi  21221  ptpjopn  21225  txdis1cn  21248  txtube  21253  txcmplem1  21254  hausdiag  21258  tx1stc  21263  txkgen  21265  xkococnlem  21272  xkococn  21273  elqtop  21310  kqreglem1  21354  elmptrab  21440  isfbas  21443  elflim2  21578  elflim  21585  hauspwpwf1  21601  alexsublem  21658  ghmcnp  21728  qustgplem  21734  tsmssubm  21756  elutop  21847  ustuqtop4  21858  isucn  21892  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  ismet2  21948  imasdsf1olem  21988  blres  22046  elmopn  22057  mopni  22107  neibl  22116  nrmmetd  22189  ngppropd  22251  elcncf  22500  mulc1cncf  22516  elpi1  22653  isclmp  22705  metcld2  22913  pmltpclem1  23024  ovolval  23049  itg1climres  23287  itg2val  23301  isibl  23338  itgeq1f  23344  itgresr  23351  iblcn  23371  itgfsum  23399  dvreslem  23479  dvfsumlem2  23594  deg1ldg  23656  vieta1  23871  ulm2  23943  sincosq2sgn  24055  sincosq4sgn  24057  efopn  24204  dvdsflsumcom  24714  fsumvma2  24739  logfac2  24742  dchrptlem1  24789  lgsdchrval  24879  2lgslem1a  24916  pntibndlem3  25081  pntlemi  25093  pntleme  25097  pnt3  25101  istrkgld  25158  istrkg2ld  25159  istrkg3ld  25160  axtgsegcon  25163  axtg5seg  25164  axtgpasch  25166  axtgupdim2  25170  legov  25280  islnopp  25431  ishpg  25451  iscgra1  25502  brcgr  25580  brbtwn2  25585  axsegconlem1  25597  axsegcon  25607  axcontlem10  25653  usgra2edg  25911  trls  26066  istrl2  26068  trlon  26070  is2wlk  26095  spths  26097  0spth  26101  pthon  26105  spthon  26112  isspthonpth  26114  usgra2wlkspthlem1  26147  0crct  26154  0cycl  26155  usgrcyclnl2  26169  wwlknprop  26214  vfwlkniswwlkn  26234  wwlknext  26252  wwlknfi  26266  clwlk  26281  isclwlk  26284  clwlkcompim  26292  clwwlkn2  26303  clwwlknimp  26304  clwwlkel  26321  clwwlkf  26322  clwwlkext2edg  26330  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  erclwwlknsym  26354  erclwwlkntr  26355  clwlkfoclwwlk  26372  el2wlkonotot0  26399  2spontn0vne  26414  rusgranumwlkl1  26474  rusgranumwlklem3  26478  rusgranumwlkb0  26480  rusgra0edg  26482  eupath2lem2  26505  3cyclfrgrarn1  26539  4cycl2vnunb  26544  frg2wot1  26584  usg2spot2nb  26592  extwwlkfablem2  26605  numclwwlkovfel2  26610  numclwwlkovf2  26611  numclwwlkovf2ex  26613  numclwwlkovgel  26615  numclwwlkovgelim  26616  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  numclwwlk5  26639  vciOLD  26800  isvclem  26816  nmoofval  27001  isph  27061  norm3lemt  27393  isch2  27464  cmbr  27827  eigre  28078  eigorth  28081  nmopub  28151  nmfnleub  28168  cvbr  28525  mdbr  28537  dmdbr  28542  chrelat2  28613  mdsymlem2  28647  rexunirn  28715  ifeqeqx  28745  funcnvmptOLD  28850  funcnvmpt  28851  1stpreima  28867  fpwrelmapffslem  28895  isomnd  29032  archirng  29073  isslmd  29086  slmdlema  29087  orngmul  29134  dya2iocuni  29672  omsfval  29683  elcarsg  29694  itgeq12dv  29715  isrrvv  29832  istrkg2d  29997  axtgupdim2OLD  29999  brafs  30003  bnj956  30101  bnj1146  30116  bnj18eq1  30251  kur14  30452  pconcn  30460  cnpcon  30466  txpcon  30468  cvmscbv  30494  cvmcov  30499  cvmsi  30501  cvmsval  30502  cvmopnlem  30514  cvmlift2lem10  30548  cvmlift3lem2  30556  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  cvmlift3  30564  mclsssvlem  30713  mclsind  30721  eldm3  30905  opelco3  30923  fv1stcnv  30925  fv2ndcnv  30926  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon2  30941  poseq  30994  soseq  30995  sltval  31044  nodenselem5  31084  nocvxminlem  31089  elfuns  31192  brsuccf  31218  brofs  31282  5segofs  31283  brifs  31320  ifscgr  31321  brcolinear  31336  lineext  31353  brfs  31356  fscgr  31357  linecgr  31358  btwnconn1lem4  31367  btwnconn1lem8  31371  btwnconn1lem11  31374  btwnconn1lem12  31375  segcon2  31382  brsegle  31385  outsideofeq  31407  funray  31417  funline  31419  fvline  31421  linethru  31430  trer  31480  finminlem  31482  ivthALT  31500  filnetlem4  31546  knoppndvlem21  31693  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axsep  31981  bj-eleq1w  32040  bj-ax8  32080  bj-rabeqd  32108  bj-axsep2  32113  csboprabg  32352  topdifinffinlem  32371  icoreval  32377  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  wl-ax11-lem8  32548  curf  32557  ptrest  32578  poimirlem1  32580  poimirlem13  32592  poimirlem14  32593  poimirlem22  32601  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  heicant  32614  mblfinlem3  32618  mblfinlem4  32619  mbfresfi  32626  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  areacirclem5  32674  cover2  32678  cover2g  32679  fdc  32711  fdc1  32712  heibor1  32779  bfp  32793  rngosn3  32893  drngoi  32920  isdrngo1  32925  isriscg  32953  isfldidl2  33038  islshpat  33322  lcvbr  33326  lshpsmreu  33414  ldual1dim  33471  cvrval  33574  cvrnbtwn3  33581  iscvlat2N  33629  ishlat3N  33659  hlrelat5N  33705  3dim0  33761  llnexatN  33825  islpln5  33839  islvol5  33883  pmapjat1  34157  ltrnu  34425  cdleme02N  34527  cdlemg33b  35013  cdlemg33c  35014  dvhb1dimN  35292  dibelval3  35454  dibopelval3  35455  dib1dim  35472  dibglbN  35473  diblsmopel  35478  dicval  35483  dicopelval  35484  dicelval3  35487  dicelval1sta  35494  dihopelvalcpre  35555  dih1dimatlem  35636  dihpN  35643  dihjatcclem4  35728  lpolsetN  35789  mapdpglem3  35982  hdmapglem7a  36237  mrefg2  36288  mzpclval  36306  eldiophb  36338  eldioph2lem1  36341  eldioph3  36347  lzenom  36351  diophin  36354  eldiophss  36356  diophrex  36357  eq0rabdioph  36358  pellexlem3  36413  elpell1qr  36429  elpell14qr  36431  elpell1234qr  36433  jm2.27  36593  rmydioph  36599  expdiophlem1  36606  expdioph  36608  pw2f1ocnv  36622  hbtlem1  36712  hbtlem7  36714  dgraalem  36734  dgraaub  36737  ifpbi2  36830  inintabd  36904  cnvcnvintabd  36925  cnvintabd  36928  clcnvlem  36949  iunrelexpmin1  37019  uneqsn  37341  k0004lem2  37466  binomcxplemnotnn0  37577  2sbc6g  37638  2sbc5g  37639  iotasbc  37642  dropab1  37672  dropab2  37673  cbvmpt21  38306  disjinfi  38375  mapsnend  38386  dmrelrnrel  38414  mullimc  38683  mullimcf  38690  fourierdlem42  39042  fourierdlem48  39047  fourierdlem50  39049  fourierdlem51  39050  fourierdlem54  39053  fourierdlem86  39085  ovnval2  39435  ovnsubaddlem1  39460  hoiqssbl  39515  vonicclem2  39575  dfdfat2  39860  pfxeq  40267  mptmpt2opabbrd  40335  2ffzoeq  40361  edgassv2  40425  uhgr2edg  40435  isfusgrf1  40539  edgnbusgreu  40595  cplgr3v  40657  vtxdun  40696  upgr2wlk  40876  upgrtrls  40909  upgristrl  40910  upgrf1istrl  40911  2pthnloop  40937  usgr2pth  40970  isclWlke  40984  isclWlkupgr  40985  iswwlksnx  41042  wlknewwlksn  41084  wwlksnfi  41112  wspthsnwspthsnon  41122  2pthon3v-av  41150  wwlks2onv  41158  elwwlks2on  41162  wpthswwlks2on  41164  rusgrnumwwlkl1  41172  rusgrnumwwlkb0  41174  clwwlksel  41221  clwwlksf  41222  erclwwlksnsym  41254  erclwwlksntr  41255  clwlksfoclwwlk  41270  0Trl  41290  0spth-av  41294  0clWlk  41298  0Crct  41300  0Cycl  41301  upgr4cycl4dv4e  41352  iseupthf1o  41369  upgriseupth  41375  eupth2lem2  41387  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  frgr2wwlk1  41494  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  av-extwwlkfablem2  41510  av-numclwwlkovfel2  41514  av-numclwwlk5  41542  mgmhmpropd  41575  ismhm0  41595  isrnghm  41682  rngcsect  41772  rngcinv  41773  rngcsectALTV  41784  rngcinvALTV  41785  ringcsect  41823  ringcinv  41824  ringcsectALTV  41847  ringcinvALTV  41848  lmod1  42075  elbigo2  42144