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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3587  r19.27m  3623  ifbi  3661  preq12bg  3898  opeq2  3905  ralunsn  3923  intab  3999  disjiun  4125  brimralrspcev  4190  opabbid  4196  opthg  4378  pocl  4448  ordelord  4526  ordtriexmid  4668  ontr2exmid  4672  onsucsssucexmid  4674  tfisi  4734  xpeq2  4789  rabxp  4812  vtoclr  4823  opeliunxp  4830  posng  4847  opbrop  4854  rexiunxp  4922  elrnmpt1  5033  dfres2  5115  brcodir  5175  poltletr  5188  xp11m  5226  elxp4  5275  elxp5  5276  dffun4f  5393  fununi  5449  fneq2  5470  fnun  5489  feq3  5518  foeq3  5613  funfveu  5708  funbrfv  5739  ssimaexg  5765  fvopab3g  5778  fvopab3ig  5779  fvelrn  5839  fmptco  5874  fsn2  5882  elunirn  5972  isoeq2  6008  isoeq3  6009  isocnv2  6018  isoini  6024  isopolem  6028  f1oiso  6032  f1oiso2  6033  oprabbid  6141  cbvoprab3  6164  mpomptx  6179  mpofun  6190  ov  6208  ovi3  6226  ov6g  6227  ovg  6228  caoftrn  6335  uchoice  6371  f1o2ndf1  6464  xporderlem  6467  f1od2  6471  suppimacnvfn  6486  brtpos2  6522  brtposg  6525  dftpos4  6534  recseq  6577  tfrlem3-2d  6583  tfrlemi1  6603  tfrexlem  6605  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  freceq1  6663  freceq2  6664  frecsuc  6678  nnaordex  6801  brecop  6899  eroveu  6900  erovlem  6901  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3qlem2  6912  th3q  6914  elpmg  6938  ixpsnval  6983  ixpsnf1o  7018  domeng  7036  dom2lem  7058  mapsnend  7099  modom  7108  xpcomco  7124  xpassen  7128  xpdom2  7129  xpf1o  7144  phplem3g  7157  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  diffifi  7198  fiintim  7238  opabfi  7247  fidcenumlemrk  7271  fidcenumlemr  7272  supeq2  7329  nninfninc  7463  nnnninfeq2  7469  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  isacnm  7559  acfun  7563  2omotaplemap  7623  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  recexnq  7757  recmulnqg  7758  ltsonq  7765  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  elinp  7841  prdisj  7859  prarloclem3  7864  prarloc  7870  distrlem5prl  7953  distrlem5pru  7954  ltexprlemell  7965  ltexprlemelu  7966  recexprlemm  7991  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  lttrsr  8129  recexgt0sr  8140  mulgt0sr  8145  ltresr  8206  axprecex  8247  axpre-lttrn  8251  axpre-mulgt0  8254  eqlelt  8412  lesub0  8807  apreap  8915  apreim  8931  aprcl  8974  aptap  8978  zltlen  9724  prime  9745  fzind  9761  qltlen  10040  xltnegi  10237  ixxval  10298  fzval  10413  fzdifsuc  10488  elfzm11  10498  elfzo  10556  zsupcllemex  10663  exbtwnzlemshrink  10683  rebtwn2zlemshrink  10688  facwordi  11178  zfz1iso  11293  pfxsuff1eqwrdeq  11471  wrd2ind  11495  shftfvalg  11583  shftfibg  11585  shftfval  11586  shftfib  11588  shftfn  11589  2shfti  11596  cau3lem  11880  caubnd2  11883  xrmaxiflemcom  12015  clim  12047  clim2  12049  climi  12053  climcn2  12075  addcn2  12076  subcn2  12077  mulcn2  12078  summodclem2a  12148  summodc  12150  fsum3  12154  fsumsplitf  12175  prodfdivap  12314  ntrivcvgap0  12316  prodeq1f  12319  prodeq2w  12323  prodeq2  12324  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodntrivap  12351  fproddivapf  12398  fprodsplitf  12399  fprodsplit1f  12401  sinbnd  12519  cosbnd  12520  divalgb  12692  ndvdssub  12697  gcdval  12736  gcdneg  12759  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemex  12778  dfgcd2  12791  gcdass  12792  algcvgblem  12827  lcmval  12841  lcmneg  12852  lcmgcdlem  12855  lcmass  12863  qredeq  12874  prmind2  12898  euclemma  12924  pw2dvdslemn  12943  qnumval  12963  qdenval  12964  pceu  13074  pczpre  13076  pcdiv  13081  prmpwdvds  13134  gzsumress  13712  gzsum0  13713  mnd1  13762  grp1  13911  qusgrp2  13916  nmznsg  14016  releqgg  14023  eqgex  14024  iscmnd  14101  gsumvalfi  14152  prdsex  14172  issrg  14269  iscrng2  14319  qusring2  14371  opprunitd  14417  crngunit  14418  dfrhm2  14461  rhmopp  14483  issubrng  14507  resrhm2b  14557  islmod  14627  lsssetm  14693  lsspropdg  14768  ixpsnbasval  14803  basis2  15149  eltg2  15154  isnei  15245  isneip  15247  restbasg  15269  iscnp  15300  iscnp3  15304  tgcn  15309  icnpimaex  15312  lmbrf  15316  cncnp  15331  cnptoprest2  15341  txbas  15359  txcnp  15372  imasnopn  15400  ispsmet  15424  ismet  15445  isxmet  15446  ismet2  15455  blres  15535  metcnp3  15612  txmetcnp  15619  mulcncf  15709  ellimc3apf  15761  limcdifap  15763  limcmpted  15764  limccnp2lem  15777  dvmptfsum  15826  elply2  15836  sincosq3sgn  15929  pellexlem3  16093  lgsquadlem1  16196  2sqlem8  16242  2sqlem9  16243  eupthres  16698  eupth2lem3lem6fi  16712  subctctexmid  17030  wexmiddifxy  17046  nnnninfex  17065