Theorem anbi2d 461

Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

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

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32d 447	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2  464  anbi1cd  465  anbi12d  470  bi2anan9  601  dn1dc  955  xorbi2d  1375  dfbi3dc  1392  xordidc  1394  eleq2w  2232  eleq2  2234  ceqsex2  2770  ceqsex6v  2774  vtocl2gaf  2797  ceqsrex2v  2862  mob2  2910  eqreu  2922  nelrdva  2937  dfss4st  3360  undif4  3476  r19.27m  3509  ifbi  3545  preq12bg  3758  opeq2  3764  ralunsn  3782  intab  3858  disjiun  3982  brimralrspcev  4046  opabbid  4052  opthg  4221  pocl  4286  ordelord  4364  ordtriexmid  4503  ontr2exmid  4507  onsucsssucexmid  4509  tfisi  4569  xpeq2  4624  rabxp  4646  vtoclr  4657  opeliunxp  4664  posng  4681  opbrop  4688  rexiunxp  4751  elrnmpt1  4860  dfres2  4941  brcodir  4996  poltletr  5009  xp11m  5047  elxp4  5096  elxp5  5097  dffun4f  5212  fununi  5264  fneq2  5285  fnun  5302  feq3  5330  foeq3  5416  funfveu  5507  funbrfv  5533  ssimaexg  5556  fvopab3g  5567  fvopab3ig  5568  fvelrn  5624  fmptco  5659  fsn2  5667  elunirn  5742  isoeq2  5778  isoeq3  5779  isocnv2  5788  isoini  5794  isopolem  5798  f1oiso  5802  f1oiso2  5803  oprabbid  5903  cbvoprab3  5926  mpomptx  5941  mpofun  5952  ov  5969  ovi3  5986  ov6g  5987  ovg  5988  caoftrn  6083  f1o2ndf1  6204  xporderlem  6207  f1od2  6211  brtpos2  6227  brtposg  6230  dftpos4  6239  recseq  6282  tfrlem3-2d  6288  tfrlemi1  6308  tfrexlem  6310  tfr1onlemaccex  6324  tfrcllemaccex  6337  tfrcl  6340  freceq1  6368  freceq2  6369  frecsuc  6383  nnaordex  6503  brecop  6599  eroveu  6600  erovlem  6601  ecopovtrn  6606  ecopovtrng  6609  th3qlem1  6611  th3qlem2  6612  th3q  6614  elpmg  6638  ixpsnval  6675  ixpsnf1o  6710  domeng  6726  dom2lem  6746  xpcomco  6800  xpassen  6804  xpdom2  6805  xpf1o  6818  phplem3g  6830  ssfiexmid  6850  domfiexmid  6852  findcard2  6863  findcard2s  6864  findcard2d  6865  findcard2sd  6866  diffifi  6868  fiintim  6902  fidcenumlemrk  6927  fidcenumlemr  6928  supeq2  6962  nnnninfeq2  7101  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  acfun  7171  ccfunen  7213  recexnq  7339  recmulnqg  7340  ltsonq  7347  enq0sym  7381  enq0ref  7382  enq0tr  7383  enq0breq  7385  addnq0mo  7396  mulnq0mo  7397  addnnnq0  7398  mulnnnq0  7399  elinp  7423  prdisj  7441  prarloclem3  7446  prarloc  7452  distrlem5prl  7535  distrlem5pru  7536  ltexprlemell  7547  ltexprlemelu  7548  recexprlemm  7573  addsrmo  7692  mulsrmo  7693  addsrpr  7694  mulsrpr  7695  lttrsr  7711  recexgt0sr  7722  mulgt0sr  7727  ltresr  7788  axprecex  7829  axpre-lttrn  7833  axpre-mulgt0  7836  eqlelt  7993  lesub0  8385  apreap  8493  apreim  8509  aprcl  8552  zltlen  9277  prime  9298  fzind  9314  qltlen  9586  xltnegi  9779  ixxval  9840  fzval  9954  fzdifsuc  10024  elfzm11  10034  elfzo  10092  exbtwnzlemshrink  10192  rebtwn2zlemshrink  10197  facwordi  10661  zfz1iso  10763  shftfvalg  10769  shftfibg  10771  shftfval  10772  shftfib  10774  shftfn  10775  2shfti  10782  cau3lem  11065  caubnd2  11068  xrmaxiflemcom  11199  clim  11231  clim2  11233  climi  11237  climcn2  11259  addcn2  11260  subcn2  11261  mulcn2  11262  summodclem2a  11331  summodc  11333  fsum3  11337  fsumsplitf  11358  prodfdivap  11497  ntrivcvgap0  11499  prodeq1f  11502  prodeq2w  11506  prodeq2  11507  prodmodc  11528  zproddc  11529  fprodseq  11533  fprodntrivap  11534  fproddivapf  11581  fprodsplitf  11582  fprodsplit1f  11584  sinbnd  11702  cosbnd  11703  divalgb  11871  ndvdssub  11876  zsupcllemex  11888  gcdval  11901  gcdneg  11924  bezoutlemstep  11939  bezoutlemmain  11940  bezoutlemex  11943  dfgcd2  11956  gcdass  11957  algcvgblem  11990  lcmval  12004  lcmneg  12015  lcmgcdlem  12018  lcmass  12026  qredeq  12037  prmind2  12061  euclemma  12087  pw2dvdslemn  12106  qnumval  12126  qdenval  12127  pceu  12236  pczpre  12238  pcdiv  12243  prmpwdvds  12294  mnd1  12666  basis2  12799  eltg2  12806  isnei  12897  isneip  12899  restbasg  12921  iscnp  12952  iscnp3  12956  tgcn  12961  icnpimaex  12964  lmbrf  12968  cncnp  12983  cnptoprest2  12993  txbas  13011  txcnp  13024  imasnopn  13052  ispsmet  13076  ismet  13097  isxmet  13098  ismet2  13107  blres  13187  metcnp3  13264  txmetcnp  13271  mulcncf  13344  ellimc3apf  13382  limcdifap  13384  limcmpted  13385  limccnp2lem  13398  sincosq3sgn  13502  2sqlem8  13712  2sqlem9  13713  subctctexmid  13994