Theorem anbi2d 468

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi2  471  anbi1cd  472  anbi12d  477  bi2anan9  614  dn1dc  973  dfifp3dc  995  ifpdfbidc  998  xorbi2d  1429  dfbi3dc  1446  xordidc  1448  eleq2w  2300  eleq2  2302  ceqsex2  2863  ceqsex6v  2867  vtocl2gaf  2890  ceqsrex2v  2958  mob2  3006  eqreu  3018  nelrdva  3033  dfss4st  3464  undif4  3586  r19.27m  3620  ifbi  3658  preq12bg  3893  opeq2  3900  ralunsn  3918  intab  3994  disjiun  4120  brimralrspcev  4185  opabbid  4191  opthg  4373  pocl  4443  ordelord  4521  ordtriexmid  4663  ontr2exmid  4667  onsucsssucexmid  4669  tfisi  4729  xpeq2  4784  rabxp  4807  vtoclr  4818  opeliunxp  4825  posng  4842  opbrop  4849  rexiunxp  4917  elrnmpt1  5028  dfres2  5110  brcodir  5170  poltletr  5183  xp11m  5221  elxp4  5270  elxp5  5271  dffun4f  5388  fununi  5444  fneq2  5465  fnun  5484  feq3  5513  foeq3  5608  funfveu  5703  funbrfv  5733  ssimaexg  5759  fvopab3g  5772  fvopab3ig  5773  fvelrn  5830  fmptco  5865  fsn2  5873  elunirn  5962  isoeq2  5998  isoeq3  5999  isocnv2  6008  isoini  6014  isopolem  6018  f1oiso  6022  f1oiso2  6023  oprabbid  6131  cbvoprab3  6154  mpomptx  6169  mpofun  6180  ov  6198  ovi3  6216  ov6g  6217  ovg  6218  caoftrn  6325  uchoice  6361  f1o2ndf1  6454  xporderlem  6457  f1od2  6461  suppimacnvfn  6476  brtpos2  6512  brtposg  6515  dftpos4  6524  recseq  6567  tfrlem3-2d  6573  tfrlemi1  6593  tfrexlem  6595  tfr1onlemaccex  6609  tfrcllemaccex  6622  tfrcl  6625  freceq1  6653  freceq2  6654  frecsuc  6668  nnaordex  6791  brecop  6889  eroveu  6890  erovlem  6891  ecopovtrn  6896  ecopovtrng  6899  th3qlem1  6901  th3qlem2  6902  th3q  6904  elpmg  6928  ixpsnval  6973  ixpsnf1o  7008  domeng  7026  dom2lem  7048  mapsnend  7089  modom  7098  xpcomco  7114  xpassen  7118  xpdom2  7119  xpf1o  7134  phplem3g  7147  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  findcard2  7183  findcard2s  7184  findcard2d  7185  findcard2sd  7186  diffifi  7188  fiintim  7228  opabfi  7237  fidcenumlemrk  7261  fidcenumlemr  7262  supeq2  7319  nninfninc  7453  nnnninfeq2  7459  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  isacnm  7549  acfun  7553  2omotaplemap  7613  2omotaplemst  7614  exmidapne  7616  ccfunen  7620  recexnq  7747  recmulnqg  7748  ltsonq  7755  enq0sym  7789  enq0ref  7790  enq0tr  7791  enq0breq  7793  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  mulnnnq0  7807  elinp  7831  prdisj  7849  prarloclem3  7854  prarloc  7860  distrlem5prl  7943  distrlem5pru  7944  ltexprlemell  7955  ltexprlemelu  7956  recexprlemm  7981  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  lttrsr  8119  recexgt0sr  8130  mulgt0sr  8135  ltresr  8196  axprecex  8237  axpre-lttrn  8241  axpre-mulgt0  8244  eqlelt  8402  lesub0  8797  apreap  8905  apreim  8921  aprcl  8964  aptap  8968  zltlen  9703  prime  9724  fzind  9740  qltlen  10019  xltnegi  10216  ixxval  10277  fzval  10392  fzdifsuc  10466  elfzm11  10476  elfzo  10534  zsupcllemex  10641  exbtwnzlemshrink  10661  rebtwn2zlemshrink  10666  facwordi  11156  zfz1iso  11271  pfxsuff1eqwrdeq  11449  wrd2ind  11473  shftfvalg  11561  shftfibg  11563  shftfval  11564  shftfib  11566  shftfn  11567  2shfti  11574  cau3lem  11858  caubnd2  11861  xrmaxiflemcom  11993  clim  12025  clim2  12027  climi  12031  climcn2  12053  addcn2  12054  subcn2  12055  mulcn2  12056  summodclem2a  12126  summodc  12128  fsum3  12132  fsumsplitf  12153  prodfdivap  12292  ntrivcvgap0  12294  prodeq1f  12297  prodeq2w  12301  prodeq2  12302  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodntrivap  12329  fproddivapf  12376  fprodsplitf  12377  fprodsplit1f  12379  sinbnd  12497  cosbnd  12498  divalgb  12670  ndvdssub  12675  gcdval  12714  gcdneg  12737  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemex  12756  dfgcd2  12769  gcdass  12770  algcvgblem  12805  lcmval  12819  lcmneg  12830  lcmgcdlem  12833  lcmass  12841  qredeq  12852  prmind2  12876  euclemma  12902  pw2dvdslemn  12921  qnumval  12941  qdenval  12942  pceu  13052  pczpre  13054  pcdiv  13059  prmpwdvds  13112  gzsumress  13689  gzsum0  13690  mnd1  13739  grp1  13888  qusgrp2  13893  nmznsg  13993  releqgg  14000  eqgex  14001  iscmnd  14078  gsumvalfi  14129  prdsex  14149  issrg  14243  iscrng2  14293  qusring2  14344  opprunitd  14390  crngunit  14391  dfrhm2  14434  rhmopp  14456  issubrng  14480  resrhm2b  14530  islmod  14600  lsssetm  14665  lsspropdg  14740  ixpsnbasval  14775  basis2  15072  eltg2  15077  isnei  15168  isneip  15170  restbasg  15192  iscnp  15223  iscnp3  15227  tgcn  15232  icnpimaex  15235  lmbrf  15239  cncnp  15254  cnptoprest2  15264  txbas  15282  txcnp  15295  imasnopn  15323  ispsmet  15347  ismet  15368  isxmet  15369  ismet2  15378  blres  15458  metcnp3  15535  txmetcnp  15542  mulcncf  15632  ellimc3apf  15684  limcdifap  15686  limcmpted  15687  limccnp2lem  15700  dvmptfsum  15749  elply2  15759  sincosq3sgn  15852  pellexlem3  16007  lgsquadlem1  16110  2sqlem8  16156  2sqlem9  16157  eupthres  16612  eupth2lem3lem6fi  16626  subctctexmid  16944  nnnninfex  16970