Theorem anbi1d 630

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 577	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  631  anbi1  632  pm5.71  1028  cador  1605  drsb1  2503  eleq1w  2827  eleq1d  2829  clelab  2890  rexeqfOLD  3363  rmoeq1OLD  3427  reueq1OLD  3428  rmoeq1f  3431  rabeq  3458  rabeqbidva  3460  rabeqd  3473  rabeqf  3480  cgsex4gOLD  3539  vtocl2gafOLD  3592  vtocl4gaOLD  3600  alexeqg  3664  reu2eqd  3758  sbc2or  3813  sbc5ALT  3833  rexss  4084  psstr  4130  difin2  4320  r19.28z  4521  dfif6  4551  rabsneq  4666  rexreusng  4703  reurexprg  4729  rabsnifsb  4747  ssunsn2  4852  preq12bg  4878  opeq1  4897  eluni  4934  csbuni  4960  unissb  4963  iuneq12d  5044  disjxun  5164  unopab  5248  mpteq12da  5251  mpteq12f  5254  mpteq12dva  5255  dftr2c  5286  axrep1  5304  axreplem  5305  zfrepclf  5312  axsepgfromrep  5315  axsepg  5318  zfauscl  5319  reusv2lem4  5419  rabxfrd  5435  opthg  5497  otthg  5505  copsexgw  5510  copsexg  5511  opeqsng  5522  euotd  5532  elopabw  5545  pocl  5615  poclOLD  5616  xpeq1  5714  elxpi  5722  vtoclr  5763  opbrop  5797  dmopab2rex  5942  resopab2  6065  dflim2  6452  dffun2  6583  fun11  6652  feq2  6729  f1eq2  6813  f1eq3  6814  foeq2  6831  brprcneu  6910  brprcneuALT  6911  ssimaexg  7008  dmfco  7018  fndmdif  7075  respreima  7099  isoeq5  7357  isoini  7374  isopolem  7381  f1oiso  7387  f1oiso2  7388  imaeqsexvOLD  7399  riotaeqdv  7405  oprabidw  7479  oprabid  7480  oprabv  7510  mpoeq123  7522  mpoeq123dva  7524  0mpo0  7533  eloprabga  7558  eloprabgaOLD  7559  resoprab  7568  resoprab2  7569  elrnmpores  7588  ov  7594  ov3  7613  ov6g  7614  ovg  7615  imaeqexov  7688  caoftrn  7753  uniuni  7797  limuni3  7889  elxp4  7962  elxp5  7963  opabex3d  8006  opabex3rd  8007  opabex3  8008  releldmdifi  8086  opiota  8100  eloprabi  8104  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabbrdOLDOLD  8124  cnvf1o  8152  frxp  8167  xporderlem  8168  poxp  8169  fnwelem  8172  poxp2  8184  xpord3pred  8193  poseq  8199  soseq  8200  suppimacnv  8215  rexsupp  8223  mpocurryd  8310  smoel2  8419  omeu  8641  oeeui  8658  omabs  8707  omopth  8718  eldifsucnn  8720  qliftel  8858  brecop  8868  eroveu  8870  erov  8872  ecopovtrn  8878  ixpsnf1o  8996  dom2lem  9052  mapsnend  9101  xpsnen  9121  xpassen  9132  pw2f1olem  9142  xpf1o  9205  unxpdom  9316  domunfican  9389  preleqALT  9686  zfinf  9708  cantnfs  9735  brttrcl  9782  ttrclselem2  9795  tcvalg  9807  r0weon  10081  fseqenlem1  10093  acni2  10115  aceq1  10186  aceq0  10187  dfac5lem4  10195  dfac2a  10199  dfac12lem2  10214  cardcf  10321  cfeq0  10325  cfsuc  10326  cff1  10327  cfss  10334  isf32lem5  10426  fin1a2lem6  10474  zfac  10529  brdom7disj  10600  brdom6disj  10601  axrepnd  10663  axunndlem1  10664  axinfnd  10675  axacndlem5  10680  axacnd  10681  zfcndrep  10683  zfcndinf  10687  zfcndac  10688  pwfseqlem4a  10730  pwfseqlem4  10731  gruina  10887  grothomex  10898  ordpipq  11011  elnpi  11057  genpass  11078  ltprord  11099  reclem2pr  11117  reclem3pr  11118  recexpr  11120  addsrmo  11142  mulsrmo  11143  addsrpr  11144  mulsrpr  11145  ltsosr  11163  mulgt0sr  11174  supsr  11181  ltresr  11209  axpre-lttrn  11235  axpre-mulgt0  11237  prime  12724  peano5uzti  12733  rexuz  12963  ltxr  13178  qbtwnre  13261  xmulneg1  13331  supxr2  13376  ixxval  13415  fzval  13569  preduz  13707  nn0opth2  14321  hashbclem  14501  hashf1lem2  14505  eqwrd  14605  pfxeq  14744  wrd2ind  14771  cshwcsh2id  14877  eqwrds3  15010  cleq1lem  15031  rtrclreclem3  15109  rtrclreclem4  15110  relexpindlem  15112  abslt  15363  absle  15364  lenegsq  15369  abs2difabs  15383  ello12  15562  elo12  15573  o1lo1  15583  rlimuni  15596  lo1resb  15610  o1resb  15612  2clim  15618  rlimcn3  15636  climcn2  15639  addcn2  15640  mulcn2  15642  o1of2  15659  sumeq1  15737  fsum2dlem  15818  modfsummod  15842  prodeq1f  15954  prodeq1  15955  fprod2dlem  16028  nndivdvds  16311  divalg2  16453  smupval  16534  gcdval  16542  gcdass  16594  lcmval  16639  lcmass  16661  rpexp  16769  pythagtriplem2  16864  pythagtrip  16881  vdwapun  17021  0ram  17067  ramub1lem2  17074  pwsle  17552  imasleval  17601  ismre  17648  ismri  17689  iscatd2  17739  dfiso2  17833  isssc  17881  funcpropd  17967  fullpropd  17987  fthres2b  17997  fthres2c  17998  setcsect  18156  cat1lem  18163  cat1  18164  prslem  18368  drsdir  18372  posi  18387  tosso  18489  odudlatb  18595  ipoval  18600  ipolt  18605  dirge  18673  gsumpropd2lem  18717  mgmhmpropd  18736  issgrpv  18759  issgrpn0  18760  ismhm0  18825  mhmpropd  18827  mndind  18863  mgmnsgrpex  18966  issubg3  19184  isga  19331  symgfixelq  19475  psgnfval  19542  psgnval  19549  dprdw  20054  subgdmdprd  20078  isrnghm  20467  issubrg  20599  resrhm2b  20630  rngcsect  20658  rngcinv  20659  ringcsect  20692  ringcinv  20693  drngpropd  20791  islmod  20884  lmodlema  20885  lmodprop2d  20944  lsslss  20982  lbspropd  21121  lbsacsbs  21181  znleval  21596  islbs4  21875  islinds3  21877  aspval2  21941  psrbag  21960  pf1ind  22380  mdetunilem4  22642  mdetunilem9  22647  istopg  22922  basis2  22979  tg2  22993  iscld  23056  isnei  23132  isneip  23134  neiptoptop  23160  neiptopnei  23161  neitr  23209  restlp  23212  iscn  23264  cnpval  23265  iscnp  23266  regsep  23363  1stcclb  23473  2ndc1stc  23480  2ndcctbss  23484  2ndcdisj  23485  llyi  23503  nllyi  23504  hausmapdom  23529  locfinnei  23552  comppfsc  23561  elkgen  23565  txbas  23596  txcls  23633  txcnpi  23637  ptpjopn  23641  txdis1cn  23664  txtube  23669  txcmplem1  23670  hausdiag  23674  tx1stc  23679  txkgen  23681  xkococn  23689  elqtop  23726  kqreglem1  23770  elmptrab  23856  isfbas  23858  elflim2  23993  elflim  24000  hauspwpwf1  24016  alexsublem  24073  ghmcnp  24144  qustgplem  24150  tsmssubm  24172  elutop  24263  ustuqtop4  24274  isucn  24308  iscfilu  24318  ispsmet  24335  ismet  24354  isxmet  24355  ismet2  24364  imasdsf1olem  24404  blres  24462  elmopn  24473  mopni  24526  neibl  24535  nrmmetd  24608  ngppropd  24671  elcncf  24934  mulc1cncf  24950  elpi1  25097  isclmp  25149  metcld2  25360  pmltpclem1  25502  itg1climres  25769  itg2val  25783  isibl  25820  itgeq1f  25826  itgeq1fOLD  25827  itgeq1  25828  cbvitgv  25832  itgresr  25834  iblcn  25854  itgfsum  25882  dvreslem  25964  dvfsumlem2  26087  dvfsumlem2OLD  26088  deg1ldg  26151  vieta1  26372  ulm2  26446  sincosq2sgn  26559  sincosq4sgn  26561  efopn  26718  dvdsflsumcom  27249  fsumvma2  27276  logfac2  27279  dchrptlem1  27326  lgsdchrval  27416  2lgslem1a  27453  pntibndlem3  27654  pntlemi  27666  pntleme  27670  pnt3  27674  sltval  27710  nolt02o  27758  slelttr  27820  nocvxminlem  27840  madebday  27956  sltlpss  27963  addsprop  28027  mulsproplemcbv  28159  mulsproplem1  28160  mulsprop  28174  absslt  28291  istrkgld  28485  istrkg2ld  28486  istrkg3ld  28487  axtgsegcon  28490  axtg5seg  28491  axtgpasch  28493  axtgupdim2  28497  legov  28611  islnopp  28765  ishpg  28785  iscgra1  28836  dfcgra2  28856  dfcgrg2  28889  brcgr  28933  brbtwn2  28938  axsegconlem1  28950  axsegcon  28960  axcontlem10  29006  edgssv2  29233  uhgr2edg  29243  isfusgrf1  29355  edgnbusgreu  29402  cplgr3v  29470  vtxdun  29517  upgr2wlk  29704  upgrtrls  29737  upgristrl  29738  upgrf1istrl  29739  2pthnloop  29767  usgr2pth  29800  isclwlke  29813  isclwlkupgr  29814  iswwlksnx  29873  wlknewwlksn  29920  2pthon3v  29976  elwwlks2on  29992  wpthswwlks2on  29994  rusgrnumwwlkl1  30001  rusgrnumwwlkb0  30004  clwwlknp  30069  clwwlkf  30079  erclwwlknsym  30102  erclwwlkntr  30103  clwwlknonwwlknonb  30138  0trl  30154  0spth  30158  0crct  30165  0cycl  30166  upgr4cycl4dv4e  30217  upgriseupth  30239  eupth2lem2  30251  3cyclfrgrrn1  30317  4cycl2vnunb  30322  frgrncvvdeqlem2  30332  frgr2wwlk1  30361  fusgr2wsp2nb  30366  numclwlk1lem1  30401  vciOLD  30593  isvclem  30609  nmoofval  30794  isph  30854  norm3lemt  31184  isch2  31255  cmbr  31616  eigre  31867  eigorth  31870  nmopub  31940  nmfnleub  31957  cvbr  32314  mdbr  32326  dmdbr  32331  chrelat2  32402  mdsymlem2  32436  rexunirn  32520  ifeqeqx  32565  iunrnmptss  32588  funcnvmpt  32685  ressupprn  32702  1stpreima  32718  fpwrelmapffslem  32746  isomnd  33051  archirng  33168  isslmd  33181  slmdlema  33182  urpropd  33212  orngmul  33298  lindflbs  33372  islbs5  33373  lindfpropd  33375  opprqus0g  33483  idlsrgval  33496  ressply1mon1p  33558  ccfldextdgrr  33682  constrsslem  33731  constrconj  33735  dya2iocuni  34248  omsfval  34259  elcarsg  34270  itgeq12dv  34291  isrrvv  34408  reprinrn  34595  reprdifc  34604  istrkg2d  34643  axtgupdim2ALTV  34645  brafs  34649  bnj956  34752  bnj1146  34767  bnj18eq1  34903  axsepg2  35058  axsepg2ALT  35059  zltp1ne  35077  isacycgr  35113  kur14  35184  pconncn  35192  cnpconn  35198  txpconn  35200  cvmscbv  35226  cvmcov  35231  cvmsi  35233  cvmsval  35234  cvmopnlem  35246  cvmlift2lem10  35280  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  satf0op  35345  sat1el2xp  35347  satffunlem  35369  dmopab3rexdif  35373  mclsssvlem  35530  mclsind  35538  rexxfr3dALT  35607  eldm3  35723  opelco3  35738  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  elfuns  35879  brsuccf  35905  brofs  35969  5segofs  35970  brifs  36007  ifscgr  36008  brcolinear  36023  lineext  36040  brfs  36043  fscgr  36044  linecgr  36045  btwnconn1lem4  36054  btwnconn1lem8  36058  btwnconn1lem11  36061  btwnconn1lem12  36062  segcon2  36069  brsegle  36072  outsideofeq  36094  funray  36104  funline  36106  fvline  36108  linethru  36117  disjeq12dv  36181  prodeq12sdv  36184  itgeq12sdv  36185  cbvitgvw2  36214  cbvitgdavw  36247  cbvitgdavw2  36263  trer  36282  finminlem  36284  ivthALT  36301  filnetlem4  36347  knoppndvlem21  36498  bj-zfauscl  36890  bj-elgab  36905  bj-imdirvallem  37146  csboprabg  37296  topdifinffinlem  37313  icoreval  37319  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  pibp19  37380  wl-ax11-lem8  37546  curf  37558  ptrest  37579  poimirlem1  37581  poimirlem13  37593  poimirlem14  37594  poimirlem22  37602  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  heicant  37615  mblfinlem3  37619  mblfinlem4  37620  mbfresfi  37626  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  areacirclem5  37672  cover2  37675  cover2g  37676  fdc  37705  fdc1  37706  heibor1  37770  bfp  37784  rngosn3  37884  drngoi  37911  isdrngo1  37916  isriscg  37944  isfldidl2  38029  brressn  38397  islshpat  38973  lcvbr  38977  lshpsmreu  39065  ldual1dim  39122  cvrval  39225  cvrnbtwn3  39232  iscvlat2N  39280  ishlat3N  39310  hlrelat5N  39358  3dim0  39414  llnexatN  39478  islpln5  39492  islvol5  39536  pmapjat1  39810  ltrnu  40078  cdleme02N  40179  cdlemg33b  40664  cdlemg33c  40665  dvhb1dimN  40943  dibelval3  41104  dibopelval3  41105  dib1dim  41122  dibglbN  41123  diblsmopel  41128  dicval  41133  dicopelval  41134  dicelval3  41137  dicelval1sta  41144  dihopelvalcpre  41205  dih1dimatlem  41286  dihpN  41293  dihjatcclem4  41378  lpolsetN  41439  mapdpglem3  41632  hdmapglem7a  41884  sticksstones23  42126  exfinfldd  42160  fimgmcyclem  42488  fimgmcyc  42489  fsuppind  42545  fsuppssindlem2  42547  prjspeclsp  42567  mrefg2  42663  mzpclval  42681  eldiophb  42713  eldioph2lem1  42716  eldioph3  42722  lzenom  42726  diophin  42728  eldiophss  42730  diophrex  42731  eq0rabdioph  42732  pellexlem3  42787  elpell1qr  42803  elpell14qr  42805  elpell1234qr  42807  jm2.27  42965  rmydioph  42971  expdiophlem1  42978  expdioph  42980  pw2f1ocnv  42994  hbtlem1  43080  hbtlem7  43082  dgraalem  43102  dgraaub  43105  dflim7  43235  omabs2  43294  tfsconcatfv2  43302  tfsconcat0i  43307  nadd1suc  43354  ifpbi2  43429  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  clcnvlem  43585  iunrelexpmin1  43670  uneqsn  43987  k0004lem2  44110  mnuprdlem1  44241  mnuprdlem2  44242  binomcxplemnotnn0  44325  2sbc6g  44384  2sbc5g  44385  iotasbc  44388  dropab1  44416  dropab2  44417  cbvmpo1  45000  r19.28zf  45064  disjinfi  45099  dmrelrnrel  45133  mullimc  45537  mullimcf  45544  limsuppnfd  45623  limsuppnf  45632  limsupre2  45646  limsupre2mpt  45651  limsupre3  45654  limsupre3mpt  45655  limsupre3uzlem  45656  fourierdlem42  46070  fourierdlem48  46075  fourierdlem50  46077  fourierdlem51  46078  fourierdlem54  46081  fourierdlem86  46113  ovnval2  46466  ovnsubaddlem1  46491  hoiqssbl  46546  vonicclem2  46605  f1cof1b  46992  f1ocof1ob2  46997  funressnbrafv2  47159  dfatdmfcoafv2  47169  2ffzoeq  47242  fundcmpsurbijinj  47284  ichreuopeq  47347  prproropf1olem4  47380  prprspr2  47392  prprsprreu  47393  prprreueq  47394  reuopreuprim  47400  isubgrgrim  47781  grtriprop  47792  isgrtri  47794  rngcsectALTV  47998  rngcinvALTV  47999  ringcsectALTV  48032  ringcinvALTV  48033  lmod1  48221  elbigo2  48286  rrx2vlinest  48475  i0oii  48599  io1ii  48600  lubeldm2d  48638  glbeldm2d  48639  functhinc  48712  fullthinc  48713