Theorem anbi1d 632

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 581	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anbi12d  633  anbi1  634  pm5.71  1025  cador  1610  drsb1  2513  eleq1w  2872  eleq1d  2874  rexeqf  3351  reueq1f  3352  rmoeq1f  3353  reueq1  3360  rmoeq1  3361  rabeqf  3428  rabeqiOLD  3430  rabeq  3431  cgsex4g  3486  vtocl2gaf  3524  vtocl4ga  3528  alexeqg  3592  elrabi  3623  reu2eqd  3675  sbc2or  3729  sbc5  3748  rexss  3986  psstr  4032  ineq1OLD  4132  difin2  4216  r19.28z  4401  rexreusng  4577  reurexprg  4600  rabsnifsb  4618  ssunsn2  4720  preq12bg  4744  opeq1OLD  4764  eluni  4803  csbuni  4829  disjxun  5028  mpteq12f  5113  axrep1  5155  axreplem  5156  zfrepclf  5162  axsepgfromrep  5165  axsepg  5168  zfauscl  5169  reusv2lem4  5267  rabxfrd  5283  opthg  5334  otthg  5342  copsexgw  5346  copsexg  5347  opeqsng  5358  euotd  5368  elopab  5379  pocl  5445  xpeq1  5533  elxpi  5541  vtoclr  5579  opbrop  5612  dmopab2rex  5750  resopab2  5871  dflim2  6215  fun11  6398  feq2  6469  f1eq2  6545  f1eq3  6546  foeq2  6562  brprcneu  6637  ssimaexg  6724  dmfco  6734  fndmdif  6789  respreima  6813  isoeq5  7053  isoini  7070  isopolem  7077  f1oiso  7083  f1oiso2  7084  riotaeqdv  7094  oprabidw  7166  oprabid  7167  oprabv  7193  mpoeq123  7205  mpoeq123dva  7207  eloprabga  7240  resoprab  7249  resoprab2  7250  elrnmpores  7267  ov  7273  ov3  7291  ov6g  7292  ovg  7293  caoftrn  7424  uniuni  7464  limuni3  7547  elxp4  7609  elxp5  7610  opabex3d  7648  opabex3rd  7649  opabex3  7650  releldmdifi  7726  opiota  7739  eloprabi  7743  mptmpoopabbrd  7761  cnvf1o  7789  frxp  7803  xporderlem  7804  poxp  7805  fnwelem  7808  suppimacnv  7824  rexsupp  7831  mpocurryd  7918  smoel2  7983  omeu  8194  oeeui  8211  omabs  8257  omopth  8268  qliftel  8363  brecop  8373  eroveu  8375  erov  8377  ecopovtrn  8383  ixpsnf1o  8485  dom2lem  8532  mapsnend  8571  xpsnen  8584  xpassen  8594  pw2f1olem  8604  xpf1o  8663  unxpdom  8709  domunfican  8775  preleqALT  9064  zfinf  9086  cantnfs  9113  tcvalg  9164  r0weon  9423  fseqenlem1  9435  acni2  9457  aceq1  9528  aceq0  9529  dfac2a  9540  dfac12lem2  9555  cardcf  9663  cfeq0  9667  cfsuc  9668  cff1  9669  cfss  9676  isf32lem5  9768  fin1a2lem6  9816  zfac  9871  brdom7disj  9942  brdom6disj  9943  axrepnd  10005  axunndlem1  10006  axinfnd  10017  axacndlem5  10022  axacnd  10023  zfcndrep  10025  zfcndinf  10029  zfcndac  10030  pwfseqlem4a  10072  pwfseqlem4  10073  gruina  10229  grothomex  10240  ordpipq  10353  elnpi  10399  genpass  10420  ltprord  10441  reclem2pr  10459  reclem3pr  10460  recexpr  10462  addsrmo  10484  mulsrmo  10485  addsrpr  10486  mulsrpr  10487  ltsosr  10505  mulgt0sr  10516  supsr  10523  ltresr  10551  axpre-lttrn  10577  axpre-mulgt0  10579  prime  12051  peano5uzti  12060  rexuz  12286  ltxr  12498  qbtwnre  12580  xmulneg1  12650  supxr2  12695  ixxval  12734  fzval  12887  preduz  13024  nn0opth2  13628  hashbclem  13806  hashf1lem2  13810  eqwrd  13900  pfxeq  14049  wrd2ind  14076  cshwcsh2id  14181  eqwrds3  14316  cleq1lem  14333  rtrclreclem3  14411  rtrclreclem4  14412  relexpindlem  14414  abslt  14666  absle  14667  lenegsq  14672  abs2difabs  14686  ello12  14865  elo12  14876  o1lo1  14886  rlimuni  14899  lo1resb  14913  o1resb  14915  2clim  14921  rlimcn2  14939  climcn2  14941  addcn2  14942  mulcn2  14944  o1of2  14961  sumeq1  15037  fsum2dlem  15117  modfsummod  15141  prodeq1f  15254  fprod2dlem  15326  nndivdvds  15608  divalg2  15746  smupval  15827  gcdval  15835  gcdass  15885  lcmval  15926  lcmass  15948  rpexp  16054  pythagtriplem2  16144  pythagtrip  16161  vdwapun  16300  0ram  16346  ramub1lem2  16353  pwsle  16757  imasleval  16806  ismre  16853  ismri  16894  iscatd2  16944  dfiso2  17034  isssc  17082  funcpropd  17162  fullpropd  17182  fthres2b  17192  fthres2c  17193  setcsect  17341  prslem  17533  drsdir  17537  posi  17552  tosso  17638  ipoval  17756  ipolt  17761  odudlatb  17798  dirge  17839  gsumpropd2lem  17881  issgrpv  17895  issgrpn0  17896  mhmpropd  17954  mndind  17984  mgmnsgrpex  18088  issubg3  18289  isga  18413  symgfixelq  18553  psgnfval  18620  psgnval  18627  dprdw  19125  subgdmdprd  19149  drngpropd  19522  issubrg  19528  islmod  19631  lmodlema  19632  lmodprop2d  19689  lsslss  19726  lbspropd  19864  lbsacsbs  19921  znleval  20246  islbs4  20521  islinds3  20523  aspval2  20584  psrbag  20602  pf1ind  20979  mdetunilem4  21220  mdetunilem9  21225  istopg  21500  basis2  21556  tg2  21570  iscld  21632  isnei  21708  isneip  21710  neiptoptop  21736  neiptopnei  21737  neitr  21785  restlp  21788  iscn  21840  cnpval  21841  iscnp  21842  regsep  21939  1stcclb  22049  2ndc1stc  22056  2ndcctbss  22060  2ndcdisj  22061  llyi  22079  nllyi  22080  hausmapdom  22105  locfinnei  22128  comppfsc  22137  elkgen  22141  txbas  22172  txcls  22209  txcnpi  22213  ptpjopn  22217  txdis1cn  22240  txtube  22245  txcmplem1  22246  hausdiag  22250  tx1stc  22255  txkgen  22257  xkococn  22265  elqtop  22302  kqreglem1  22346  elmptrab  22432  isfbas  22434  elflim2  22569  elflim  22576  hauspwpwf1  22592  alexsublem  22649  ghmcnp  22720  qustgplem  22726  tsmssubm  22748  elutop  22839  ustuqtop4  22850  isucn  22884  iscfilu  22894  ispsmet  22911  ismet  22930  isxmet  22931  ismet2  22940  imasdsf1olem  22980  blres  23038  elmopn  23049  mopni  23099  neibl  23108  nrmmetd  23181  ngppropd  23243  elcncf  23494  mulc1cncf  23510  elpi1  23650  isclmp  23702  metcld2  23911  pmltpclem1  24052  itg1climres  24318  itg2val  24332  isibl  24369  itgeq1f  24375  itgresr  24382  iblcn  24402  itgfsum  24430  dvreslem  24512  dvfsumlem2  24630  deg1ldg  24693  vieta1  24908  ulm2  24980  sincosq2sgn  25092  sincosq4sgn  25094  efopn  25249  dvdsflsumcom  25773  fsumvma2  25798  logfac2  25801  dchrptlem1  25848  lgsdchrval  25938  2lgslem1a  25975  pntibndlem3  26176  pntlemi  26188  pntleme  26192  pnt3  26196  istrkgld  26253  istrkg2ld  26254  istrkg3ld  26255  axtgsegcon  26258  axtg5seg  26259  axtgpasch  26261  axtgupdim2  26265  legov  26379  islnopp  26533  ishpg  26553  iscgra1  26604  dfcgra2  26624  dfcgrg2  26657  brcgr  26694  brbtwn2  26699  axsegconlem1  26711  axsegcon  26721  axcontlem10  26767  edgssv2  26988  uhgr2edg  26998  isfusgrf1  27110  edgnbusgreu  27157  cplgr3v  27225  vtxdun  27271  upgr2wlk  27458  upgrtrls  27491  upgristrl  27492  upgrf1istrl  27493  2pthnloop  27520  usgr2pth  27553  isclwlke  27566  isclwlkupgr  27567  iswwlksnx  27626  wlknewwlksn  27673  2pthon3v  27729  elwwlks2on  27745  wpthswwlks2on  27747  rusgrnumwwlkl1  27754  rusgrnumwwlkb0  27757  clwwlknp  27822  clwwlkf  27832  erclwwlknsym  27855  erclwwlkntr  27856  clwwlknonwwlknonb  27891  0trl  27907  0spth  27911  0crct  27918  0cycl  27919  upgr4cycl4dv4e  27970  upgriseupth  27992  eupth2lem2  28004  3cyclfrgrrn1  28070  4cycl2vnunb  28075  frgrncvvdeqlem2  28085  frgr2wwlk1  28114  fusgr2wsp2nb  28119  numclwlk1lem1  28154  vciOLD  28344  isvclem  28360  nmoofval  28545  isph  28605  norm3lemt  28935  isch2  29006  cmbr  29367  eigre  29618  eigorth  29621  nmopub  29691  nmfnleub  29708  cvbr  30065  mdbr  30077  dmdbr  30082  chrelat2  30153  mdsymlem2  30187  rexunirn  30263  ifeqeqx  30309  iunrnmptss  30329  funcnvmpt  30430  ressupprn  30450  1stpreima  30466  fpwrelmapffslem  30494  isomnd  30752  archirng  30867  isslmd  30880  slmdlema  30881  orngmul  30927  lindflbs  30994  lindfpropd  30996  idlsrgval  31056  ccfldextdgrr  31145  dya2iocuni  31651  omsfval  31662  elcarsg  31673  itgeq12dv  31694  isrrvv  31811  reprinrn  31999  reprdifc  32008  istrkg2d  32047  axtgupdim2ALTV  32049  brafs  32053  bnj956  32158  bnj1146  32173  bnj18eq1  32309  zltp1ne  32458  isacycgr  32505  kur14  32576  pconncn  32584  cnpconn  32590  txpconn  32592  cvmscbv  32618  cvmcov  32623  cvmsi  32625  cvmsval  32626  cvmopnlem  32638  cvmlift2lem10  32672  cvmlift3lem2  32680  cvmlift3lem6  32684  cvmlift3lem7  32685  cvmlift3lem9  32687  cvmlift3  32688  satf0op  32737  sat1el2xp  32739  satffunlem  32761  dmopab3rexdif  32765  mclsssvlem  32922  mclsind  32930  eldm3  33110  opelco3  33131  dfon2lem6  33146  dfon2lem7  33147  dfon2lem8  33148  dfon2  33150  poseq  33208  soseq  33209  sltval  33267  nolt02o  33312  slelttr  33349  nocvxminlem  33360  elfuns  33489  brsuccf  33515  brofs  33579  5segofs  33580  brifs  33617  ifscgr  33618  brcolinear  33633  lineext  33650  brfs  33653  fscgr  33654  linecgr  33655  btwnconn1lem4  33664  btwnconn1lem8  33668  btwnconn1lem11  33671  btwnconn1lem12  33672  segcon2  33679  brsegle  33682  outsideofeq  33704  funray  33714  funline  33716  fvline  33718  linethru  33727  trer  33777  finminlem  33779  ivthALT  33796  filnetlem4  33842  knoppndvlem21  33984  bj-rabeqd  34362  bj-zfauscl  34367  bj-imdirvallem  34595  csboprabg  34747  topdifinffinlem  34764  icoreval  34770  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlssretop  34780  pibp19  34831  wl-ax11-lem8  34989  curf  35035  ptrest  35056  poimirlem1  35058  poimirlem13  35070  poimirlem14  35071  poimirlem22  35079  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  heicant  35092  mblfinlem3  35096  mblfinlem4  35097  mbfresfi  35103  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  areacirclem5  35149  cover2  35152  cover2g  35153  fdc  35183  fdc1  35184  heibor1  35248  bfp  35262  rngosn3  35362  drngoi  35389  isdrngo1  35394  isriscg  35422  isfldidl2  35507  islshpat  36313  lcvbr  36317  lshpsmreu  36405  ldual1dim  36462  cvrval  36565  cvrnbtwn3  36572  iscvlat2N  36620  ishlat3N  36650  hlrelat5N  36697  3dim0  36753  llnexatN  36817  islpln5  36831  islvol5  36875  pmapjat1  37149  ltrnu  37417  cdleme02N  37518  cdlemg33b  38003  cdlemg33c  38004  dvhb1dimN  38282  dibelval3  38443  dibopelval3  38444  dib1dim  38461  dibglbN  38462  diblsmopel  38467  dicval  38472  dicopelval  38473  dicelval3  38476  dicelval1sta  38483  dihopelvalcpre  38544  dih1dimatlem  38625  dihpN  38632  dihjatcclem4  38717  lpolsetN  38778  mapdpglem3  38971  hdmapglem7a  39223  fsuppind  39456  fsuppssindlem2  39458  prjspeclsp  39606  mrefg2  39648  mzpclval  39666  eldiophb  39698  eldioph2lem1  39701  eldioph3  39707  lzenom  39711  diophin  39713  eldiophss  39715  diophrex  39716  eq0rabdioph  39717  pellexlem3  39772  elpell1qr  39788  elpell14qr  39790  elpell1234qr  39792  jm2.27  39949  rmydioph  39955  expdiophlem1  39962  expdioph  39964  pw2f1ocnv  39978  hbtlem1  40067  hbtlem7  40069  dgraalem  40089  dgraaub  40092  ifpbi2  40175  inintabd  40279  cnvcnvintabd  40300  cnvintabd  40303  clcnvlem  40323  iunrelexpmin1  40409  uneqsn  40726  k0004lem2  40851  mnuprdlem1  40980  mnuprdlem2  40981  binomcxplemnotnn0  41060  2sbc6g  41119  2sbc5g  41120  iotasbc  41123  dropab1  41151  dropab2  41152  cbvmpo1  41734  disjinfi  41820  dmrelrnrel  41856  mullimc  42258  mullimcf  42265  limsuppnfd  42344  limsuppnf  42353  limsupre2  42367  limsupre2mpt  42372  limsupre3  42375  limsupre3mpt  42376  limsupre3uzlem  42377  fourierdlem42  42791  fourierdlem48  42796  fourierdlem50  42798  fourierdlem51  42799  fourierdlem54  42802  fourierdlem86  42834  ovnval2  43184  ovnsubaddlem1  43209  hoiqssbl  43264  vonicclem2  43323  funressnbrafv2  43800  dfatdmfcoafv2  43810  2ffzoeq  43885  fundcmpsurbijinj  43927  ichreuopeq  43990  prproropf1olem4  44023  prprspr2  44035  prprsprreu  44036  prprreueq  44037  reuopreuprim  44043  mgmhmpropd  44405  ismhm0  44425  isrnghm  44516  rngcsect  44604  rngcinv  44605  rngcsectALTV  44616  rngcinvALTV  44617  ringcsect  44655  ringcinv  44656  ringcsectALTV  44679  ringcinvALTV  44680  lmod1  44901  elbigo2  44966  rrx2vlinest  45155