Theorem anbi1d 643

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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 589	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi12d  644  anbi1  645  pm5.71  1045  cador  1641  drsb1  2524  eleq1w  2843  eleq1d  2845  clelab  2904  rmoeq1f  3402  rabeq  3426  rabeqbidva  3428  rabeqd  3439  rabeqf  3445  alexeqg  3605  reu2eqd  3694  sbc2or  3748  sbc5ALT  3768  rexssOLD  4007  psstr  4056  difin2  4247  r19.28z  4458  dfif6  4485  rabsneq  4603  rexreusng  4640  reurexprg  4665  rabsnifsb  4683  ssunsn2  4788  preq12bg  4813  opeq1  4833  eluni  4870  csbuni  4898  unissb  4901  iuneq12d  4980  disjxun  5101  unopab  5185  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  dftr2c  5215  axrep1  5233  axreplem  5234  zfrepclf  5246  axsepgfromrep  5249  axsepg  5252  sepg  5253  zfausclOLD  5255  reusv2lem4  5366  rabxfrd  5382  opthg  5453  otthg  5461  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  opeqsng  5480  euotd  5490  elopabw  5504  pocl  5571  xpeq1  5669  elxpi  5677  vtoclr  5718  opbrop  5753  dmopab2rex  5901  resopab2  6032  rnco  6248  dflim2  6416  dffun2  6543  fun11  6608  feq2  6682  f1eq2  6768  f1eq3  6769  foeq2  6787  brprcneu  6869  brprcneuALT  6870  ssimaexg  6965  dmfco  6975  funcnvmpt  6989  fndmdif  7035  respreima  7059  isoeq5  7323  isoini  7340  isopolem  7347  f1oiso  7353  f1oiso2  7354  riotaeqdv  7372  oprabidw  7445  oprabid  7446  oprabv  7474  mpoeq123  7486  mpoeq123dva  7488  0mpo0  7497  eloprabga  7523  resoprab  7532  resoprab2  7533  elrnmpores  7552  ov  7558  ov3  7577  ov6g  7578  ovg  7579  imaeqexov  7653  caoftrn  7720  uniuni  7762  limuni3  7849  elxp4  7920  elxp5  7921  opabex3d  7963  opabex3rd  7964  opabex3  7965  releldmdifi  8043  opiota  8057  eloprabi  8061  mptmpoopabbrd  8081  cnvf1o  8109  frxp  8125  xporderlem  8126  poxp  8127  fnwelem  8130  poxp2  8142  xpord3pred  8151  poseq  8157  soseq  8158  suppimacnv  8173  rexsupp  8181  mpocurryd  8268  smoel2  8353  omeu  8573  oeeui  8591  omabs  8640  omopth  8651  eldifsucnn  8653  qliftel  8801  brecop  8811  eroveu  8813  erov  8815  ecopovtrn  8821  curf  8870  ixpsnf1o  8946  dom2lem  8999  mapsnend  9044  xpsnen  9060  xpassen  9070  pw2f1olem  9080  xpf1o  9138  unxpdom  9230  domunfican  9292  preleqALT  9597  zfinf  9619  cantnfs  9646  brttrcl  9693  ttrclselem2  9706  tcvalg  9716  r0weon  10016  fseqenlem1  10028  acni2  10050  aceq1  10121  aceq0  10122  dfac5lem4  10130  dfac2a  10133  dfac12lem2  10148  cardcf  10254  cfeq0  10259  cfsuc  10260  cff1  10261  cfss  10268  isf32lem5  10360  fin1a2lem6  10408  zfac  10463  brdom7disj  10535  brdom6disj  10536  axrepnd  10604  axunndlem1  10605  axinfnd  10616  axacndlem5  10621  axacnd  10622  zfcndrep  10624  zfcndinf  10628  zfcndac  10629  pwfseqlem4a  10671  pwfseqlem4  10672  gruina  10828  grothomex  10839  ordpipq  10952  elnpi  10998  genpass  11019  ltprord  11040  reclem2pr  11058  reclem3pr  11059  recexpr  11061  addsrmo  11083  mulsrmo  11084  addsrpr  11085  mulsrpr  11086  ltsosr  11104  mulgt0sr  11115  supsr  11122  ltresr  11150  axpre-lttrn  11176  axpre-mulgt0  11178  prime  12703  peano5uzti  12712  rexuz  12948  ltxr  13167  qbtwnre  13252  xmulneg1  13322  supxr2  13367  ixxval  13407  fzval  13564  preduz  13706  nn0opth2  14337  hashbclem  14518  hashf1lem2  14522  eqwrd  14623  pfxeq  14766  wrd2ind  14793  cshwcsh2id  14900  eqwrds3  15035  cleq1lem  15056  rtrclreclem3  15134  rtrclreclem4  15135  relexpindlem  15137  abslt  15403  absle  15404  lenegsq  15409  abs2difabs  15423  ello12  15604  elo12  15615  o1lo1  15625  rlimuni  15638  lo1resb  15652  o1resb  15654  2clim  15660  rlimcn3  15678  climcn2  15681  addcn2  15682  mulcn2  15684  o1of2  15701  sumeq1  15777  fsum2dlem  15857  modfsummod  15882  prodeq1f  15996  prodeq1  15997  fprod2dlem  16068  nndivdvds  16352  divalg2  16496  smupval  16579  gcdval  16587  gcdass  16638  lcmval  16683  lcmass  16705  rpexp  16814  pythagtriplem2  16910  pythagtrip  16927  vdwapun  17067  0ram  17113  ramub1lem2  17120  pwsle  17579  imasleval  17628  ismre  17675  ismri  17720  iscatd2  17770  dfiso2  17862  isssc  17910  funcpropd  17992  fullpropd  18012  fthres2b  18022  fthres2c  18023  setcsect  18179  cat1lem  18186  cat1  18187  prslem  18386  drsdir  18391  posi  18406  tosso  18506  odudlatb  18614  ipoval  18619  ipolt  18624  dirge  18692  mgmidpfod  18771  gsumpropd2lem  18782  mgmhmpropd  18801  issgrpv  18824  issgrpn0  18825  ismhm0  18899  mhmpropd  18901  mndind  18938  mgmnsgrpex  19044  issubg3  19269  isga  19419  symgfixelq  19561  psgnfval  19628  psgnval  19635  dprdw  20140  subgdmdprd  20164  isomnd  20251  isrnghm  20583  issubrg  20734  resrhm2b  20765  rngcsect  20799  rngcinv  20800  ringcsect  20833  ringcinv  20834  drngpropd  20937  orngmul  21032  islmod  21049  lmodlema  21050  lmodprop2d  21109  lsslss  21146  lbspropd  21284  lbsacsbs  21344  isfieldidl2  21451  znleval  21768  islbs4  22046  islinds3  22048  aspval2  22114  psrbag  22133  pf1ind  22581  mdetunilem4  22838  mdetunilem9  22843  istopg  23121  basis2  23177  tg2  23191  iscld  23253  isnei  23329  isneip  23331  neiptoptop  23357  neiptopnei  23358  neitr  23406  restlp  23409  iscn  23461  cnpval  23462  iscnp  23463  regsep  23560  1stcclb  23670  2ndc1stc  23677  2ndcctbss  23682  2ndcdisj  23683  llyi  23701  nllyi  23702  hausmapdom  23727  locfinnei  23750  comppfsc  23759  elkgen  23763  txbas  23794  txcls  23831  txcnpi  23835  ptpjopn  23839  txdis1cn  23862  txtube  23867  txcmplem1  23868  hausdiag  23872  tx1stc  23877  txkgen  23879  xkococn  23887  elqtop  23924  kqreglem1  23968  elmptrab  24054  isfbas  24056  elflim2  24191  elflim  24198  hauspwpwf1  24214  alexsublem  24271  ghmcnp  24342  qustgplem  24348  tsmssubm  24370  elutop  24460  ustuqtop4  24471  isucn  24504  iscfilu  24514  ispsmet  24531  ismet  24550  isxmet  24551  ismet2  24560  imasdsf1olem  24600  blres  24658  elmopn  24669  mopni  24719  neibl  24728  nrmmetd  24801  ngppropd  24864  elcncf  25118  mulc1cncf  25134  elpi1  25274  isclmp  25326  metcld2  25536  pmltpclem1  25677  itg1climres  25943  itg2val  25957  isibl  25994  itgeq1f  26000  itgeq1  26001  cbvitgv  26005  itgresr  26007  iblcn  26027  itgfsum  26055  dvreslem  26137  dvfsumlem2  26255  deg1ldg  26318  vieta1  26545  ulm2  26622  sincosq2sgn  26738  sincosq4sgn  26740  efopn  26896  dvdsflsumcom  27425  fsumvma2  27451  logfac2  27454  dchrptlem1  27501  lgsdchrval  27591  2lgslem1a  27628  pntibndlem3  27829  pntlemi  27841  pntleme  27845  pnt3  27849  ltsval  27884  nolt02o  27932  leltstr  27998  nocvxminlem  28020  madebday  28166  ltslpss  28174  addsprop  28242  mulsproplemcbv  28381  mulsproplem1  28382  mulsprop  28396  abslts  28515  eucliddivs  28642  bdayfinbndlem2  28734  z12sge0  28749  istrkgld  28801  istrkg2ld  28802  istrkg3ld  28803  axtgsegcon  28806  axtg5seg  28807  axtgpasch  28809  axtgupdim2  28813  legov  28928  islnopp  29095  ishpg  29117  iscgra1  29197  dfcgra2  29218  elcgrabasi  29255  dfcgrg2  29288  brprlng  29296  brcgr  29358  brbtwn2  29363  axsegconlem1  29375  axsegcon  29385  axcontlem10  29431  edgssv2  29659  uhgr2edg  29669  isfusgrf1  29781  edgnbusgreu  29828  cplgr3v  29896  vtxdun  29942  upgr2wlk  30127  upgrtrls  30164  upgristrl  30165  upgrf1istrl  30166  dfpth2  30194  2pthnloop  30197  usgr2pth  30230  isclwlke  30244  isclwlkupgr  30245  iswwlksnx  30309  wlknewwlksn  30356  2pthon3v  30412  elwwlks2on  30430  wpthswwlks2on  30433  rusgrnumwwlkl1  30440  rusgrnumwwlkb0  30443  clwwlknp  30508  clwwlkf  30518  erclwwlknsym  30541  erclwwlkntr  30542  clwwlknonwwlknonb  30577  0trl  30593  0spth  30597  0crct  30604  0cycl  30605  isacycgr  30631  upgr4cycl4dv4e  30666  upgriseupth  30688  eupth2lem2  30700  3cyclfrgrrn1  30766  4cycl2vnunb  30771  frgrncvvdeqlem2  30781  frgr2wwlk1  30810  fusgr2wsp2nb  30815  numclwlk1lem1  30850  vciOLD  31043  isvclem  31059  nmoofval  31244  isph  31304  norm3lemt  31634  isch2  31705  cmbr  32066  eigre  32317  eigorth  32320  nmopub  32390  nmfnleub  32407  cvbr  32764  mdbr  32776  dmdbr  32781  chrelat2  32852  mdsymlem2  32886  rexunirn  32968  ifeqeqx  33018  iunrnmptss  33039  fdifsupp  33158  ressupprn  33163  1stpreima  33180  fpwrelmapffslem  33204  archirng  33629  isslmd  33643  slmdlema  33644  urpropd  33671  lindflbs  33813  islbs5  33814  lindfpropd  33816  opprqus0g  33893  idlsrgval  33914  ressply1mon1p  33979  ccfldextdgrr  34183  constrsslem  34252  constrconj  34256  constrlccllem  34264  constrcbvlem  34266  dya2iocuni  34795  omsfval  34806  elcarsg  34817  itgeq12dv  34838  isrrvv  34955  reprinrn  35127  reprdifc  35136  istrkg2d  35175  axtgupdim2ALTV  35177  brafs  35184  bnj956  35287  bnj1146  35301  bnj18eq1  35437  axsepg2  35667  axsepg3  35668  axsepg3ALT  35669  axsepg4  35670  axsepg5  35671  zltp1ne  35715  kur14  35796  pconncn  35804  cnpconn  35810  txpconn  35812  cvmscbv  35838  cvmcov  35843  cvmsi  35845  cvmsval  35846  cvmopnlem  35858  cvmlift2lem10  35892  cvmlift3lem2  35900  cvmlift3lem6  35904  cvmlift3lem7  35905  cvmlift3lem9  35907  cvmlift3  35908  satf0op  35957  sat1el2xp  35959  satffunlem  35981  dmopab3rexdif  35985  mclsssvlem  36142  mclsind  36150  rexxfr3dALT  36219  eldm3  36341  opelco3  36355  dfon2lem6  36366  dfon2lem7  36367  dfon2lem8  36368  dfon2  36370  elfuns  36493  lemsuccf  36519  brofs  36586  5segofs  36587  brifs  36624  ifscgr  36625  brcolinear  36640  lineext  36657  brfs  36660  fscgr  36661  linecgr  36662  btwnconn1lem4  36671  btwnconn1lem8  36675  btwnconn1lem11  36678  btwnconn1lem12  36679  segcon2  36686  brsegle  36689  outsideofeq  36711  funray  36721  funline  36723  fvline  36725  linethru  36734  disjeq12dv  36836  prodeq12sdv  36839  itgeq12sdv  36840  cbvitgvw2  36869  cbvitgdavw  36902  cbvitgdavw2  36918  trer  36936  finminlem  36938  ivthALT  36955  filnetlem4  37001  axtco1  37093  axtco1from2  37095  ttcexg  37152  mh-infprim1bi  37166  knoppndvlem21  37230  bj-sepg  37668  bj-elgab  37684  bj-imdirvallem  37933  csboprabg  38085  topdifinffinlem  38102  icoreval  38108  isbasisrelowllem1  38110  isbasisrelowllem2  38111  relowlssretop  38118  pibp19  38169  ptrest  38369  poimirlem1  38371  poimirlem13  38383  poimirlem14  38384  poimirlem22  38392  poimirlem24  38394  poimirlem26  38396  poimirlem27  38397  heicant  38405  mblfinlem3  38409  mblfinlem4  38410  mbfresfi  38416  itg2addnclem3  38423  itg2addnc  38424  itg2gt0cn  38425  areacirclem5  38462  cover2  38466  cover2g  38467  fdc  38496  fdc1  38497  heibor1  38561  bfp  38575  rngosn3  38675  drngoi  38702  isdrngo1  38707  isriscg  38735  isfldidl2  38820  raldmqseu  39114  eldmxrncnvepres  39183  brressn  39280  islshpat  39891  lcvbr  39895  lshpsmreu  39983  ldual1dim  40040  cvrval  40143  cvrnbtwn3  40150  iscvlat2N  40198  ishlat3N  40228  hlrelat5N  40275  3dim0  40331  llnexatN  40395  islpln5  40409  islvol5  40453  pmapjat1  40727  ltrnu  40995  cdleme02N  41096  cdlemg33b  41581  cdlemg33c  41582  dvhb1dimN  41860  dibelval3  42021  dibopelval3  42022  dib1dim  42039  dibglbN  42040  diblsmopel  42045  dicval  42050  dicopelval  42051  dicelval3  42054  dicelval1sta  42061  dihopelvalcpre  42122  dih1dimatlem  42203  dihpN  42210  dihjatcclem4  42295  lpolsetN  42356  mapdpglem3  42549  hdmapglem7a  42801  sticksstones23  43036  exfinfldd  43070  fimgmcyclem  43416  fimgmcyc  43417  fsuppind  43437  fsuppssindlem2  43439  prjspeclsp  43459  mrefg2  43553  mzpclval  43571  eldiophb  43603  eldioph2lem1  43606  eldioph3  43612  lzenom  43616  diophin  43618  eldiophss  43620  diophrex  43621  eq0rabdioph  43622  pellexlem3  43673  elpell1qr  43689  elpell14qr  43691  elpell1234qr  43693  jm2.27  43850  rmydioph  43856  expdiophlem1  43863  expdioph  43865  pw2f1ocnv  43879  hbtlem1  43965  hbtlem7  43967  dgraalem  43987  dgraaub  43990  dflim7  44115  omabs2  44174  tfsconcatfv2  44182  tfsconcat0i  44187  nadd1suc  44234  ifpbi2  44308  inintabd  44420  cnvcnvintabd  44441  cnvintabd  44444  clcnvlem  44464  iunrelexpmin1  44549  uneqsn  44866  k0004lem2  44989  mnuprdlem1  45097  mnuprdlem2  45098  binomcxplemnotnn0  45181  2sbc6g  45240  2sbc5g  45241  iotasbc  45244  dropab1  45271  dropab2  45272  relpeq5  45772  modelaxreplem3  45804  omssaxinf2  45812  brpermmodel  45827  permaxinf2lem  45836  cbvmpo1  45931  r19.28zf  45992  disjinfi  46025  dmrelrnrel  46057  mullimc  46447  mullimcf  46454  limsuppnfd  46531  limsuppnf  46540  limsupre2  46554  limsupre2mpt  46559  limsupre3  46562  limsupre3mpt  46563  limsupre3uzlem  46564  fourierdlem42  46978  fourierdlem48  46983  fourierdlem50  46985  fourierdlem51  46986  fourierdlem54  46989  fourierdlem86  47021  ovnval2  47374  ovnsubaddlem1  47399  hoiqssbl  47454  vonicclem2  47513  f1cof1b  47966  f1ocof1ob2  47971  funressnbrafv2  48133  dfatdmfcoafv2  48143  2ffzoeq  48217  fundcmpsurbijinj  48311  ichreuopeq  48374  prproropf1olem4  48407  prprspr2  48419  prprsprreu  48420  prprreueq  48421  reuopreuprim  48427  nprmmul3  48430  isubgrgrim  48846  grtriprop  48858  isgrtri  48860  opgpgvtx  48972  pgnbgreunbgrlem1  49030  pgnbgreunbgrlem4  49036  grlimedgnedg  49048  rngcsectALTV  49191  rngcinvALTV  49192  ringcsectALTV  49225  ringcinvALTV  49226  lmod1  49423  elbigo2  49483  rrx2vlinest  49672  eloprab1st2nd  49797  i0oii  49847  io1ii  49848  lubeldm2d  49885  glbeldm2d  49886  sectpropdlem  49963  invpropdlem  49965  isopropdlem  49967  uppropd  50108  functhinc  50375  fullthinc  50377