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	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
anbi2d	|- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.32d 454	1 |- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

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  3587  r19.27m  3623  ifbi  3661  preq12bg  3896  opeq2  3903  ralunsn  3921  intab  3997  disjiun  4123  brimralrspcev  4188  opabbid  4194  opthg  4376  pocl  4446  ordelord  4524  ordtriexmid  4666  ontr2exmid  4670  onsucsssucexmid  4672  tfisi  4732  xpeq2  4787  rabxp  4810  vtoclr  4821  opeliunxp  4828  posng  4845  opbrop  4852  rexiunxp  4920  elrnmpt1  5031  dfres2  5113  brcodir  5173  poltletr  5186  xp11m  5224  elxp4  5273  elxp5  5274  dffun4f  5391  fununi  5447  fneq2  5468  fnun  5487  feq3  5516  foeq3  5611  funfveu  5706  funbrfv  5736  ssimaexg  5762  fvopab3g  5775  fvopab3ig  5776  fvelrn  5833  fmptco  5868  fsn2  5876  elunirn  5965  isoeq2  6001  isoeq3  6002  isocnv2  6011  isoini  6017  isopolem  6021  f1oiso  6025  f1oiso2  6026  oprabbid  6134  cbvoprab3  6157  mpomptx  6172  mpofun  6183  ov  6201  ovi3  6219  ov6g  6220  ovg  6221  caoftrn  6328  uchoice  6364  f1o2ndf1  6457  xporderlem  6460  f1od2  6464  suppimacnvfn  6479  brtpos2  6515  brtposg  6518  dftpos4  6527  recseq  6570  tfrlem3-2d  6576  tfrlemi1  6596  tfrexlem  6598  tfr1onlemaccex  6612  tfrcllemaccex  6625  tfrcl  6628  freceq1  6656  freceq2  6657  frecsuc  6671  nnaordex  6794  brecop  6892  eroveu  6893  erovlem  6894  ecopovtrn  6899  ecopovtrng  6902  th3qlem1  6904  th3qlem2  6905  th3q  6907  elpmg  6931  ixpsnval  6976  ixpsnf1o  7011  domeng  7029  dom2lem  7051  mapsnend  7092  modom  7101  xpcomco  7117  xpassen  7121  xpdom2  7122  xpf1o  7137  phplem3g  7150  ssfiexmid  7171  ssfiexmidt  7173  domfiexmid  7175  findcard2  7186  findcard2s  7187  findcard2d  7188  findcard2sd  7189  diffifi  7191  fiintim  7231  opabfi  7240  fidcenumlemrk  7264  fidcenumlemr  7265  supeq2  7322  nninfninc  7456  nnnninfeq2  7462  exmidfodomrlemr  7547  exmidfodomrlemrALT  7548  isacnm  7552  acfun  7556  2omotaplemap  7616  2omotaplemst  7617  exmidapne  7619  ccfunen  7623  recexnq  7750  recmulnqg  7751  ltsonq  7758  enq0sym  7792  enq0ref  7793  enq0tr  7794  enq0breq  7796  addnq0mo  7807  mulnq0mo  7808  addnnnq0  7809  mulnnnq0  7810  elinp  7834  prdisj  7852  prarloclem3  7857  prarloc  7863  distrlem5prl  7946  distrlem5pru  7947  ltexprlemell  7958  ltexprlemelu  7959  recexprlemm  7984  addsrmo  8103  mulsrmo  8104  addsrpr  8105  mulsrpr  8106  lttrsr  8122  recexgt0sr  8133  mulgt0sr  8138  ltresr  8199  axprecex  8240  axpre-lttrn  8244  axpre-mulgt0  8247  eqlelt  8405  lesub0  8800  apreap  8908  apreim  8924  aprcl  8967  aptap  8971  zltlen  9706  prime  9727  fzind  9743  qltlen  10022  xltnegi  10219  ixxval  10280  fzval  10395  fzdifsuc  10469  elfzm11  10479  elfzo  10537  zsupcllemex  10644  exbtwnzlemshrink  10664  rebtwn2zlemshrink  10669  facwordi  11159  zfz1iso  11274  pfxsuff1eqwrdeq  11452  wrd2ind  11476  shftfvalg  11564  shftfibg  11566  shftfval  11567  shftfib  11569  shftfn  11570  2shfti  11577  cau3lem  11861  caubnd2  11864  xrmaxiflemcom  11996  clim  12028  clim2  12030  climi  12034  climcn2  12056  addcn2  12057  subcn2  12058  mulcn2  12059  summodclem2a  12129  summodc  12131  fsum3  12135  fsumsplitf  12156  prodfdivap  12295  ntrivcvgap0  12297  prodeq1f  12300  prodeq2w  12304  prodeq2  12305  prodmodc  12326  zproddc  12327  fprodseq  12331  fprodntrivap  12332  fproddivapf  12379  fprodsplitf  12380  fprodsplit1f  12382  sinbnd  12500  cosbnd  12501  divalgb  12673  ndvdssub  12678  gcdval  12717  gcdneg  12740  bezoutlemstep  12755  bezoutlemmain  12756  bezoutlemex  12759  dfgcd2  12772  gcdass  12773  algcvgblem  12808  lcmval  12822  lcmneg  12833  lcmgcdlem  12836  lcmass  12844  qredeq  12855  prmind2  12879  euclemma  12905  pw2dvdslemn  12924  qnumval  12944  qdenval  12945  pceu  13055  pczpre  13057  pcdiv  13062  prmpwdvds  13115  gzsumress  13692  gzsum0  13693  mnd1  13742  grp1  13891  qusgrp2  13896  nmznsg  13996  releqgg  14003  eqgex  14004  iscmnd  14081  gsumvalfi  14132  prdsex  14152  issrg  14246  iscrng2  14296  qusring2  14347  opprunitd  14393  crngunit  14394  dfrhm2  14437  rhmopp  14459  issubrng  14483  resrhm2b  14533  islmod  14603  lsssetm  14668  lsspropdg  14743  ixpsnbasval  14778  basis2  15075  eltg2  15080  isnei  15171  isneip  15173  restbasg  15195  iscnp  15226  iscnp3  15230  tgcn  15235  icnpimaex  15238  lmbrf  15242  cncnp  15257  cnptoprest2  15267  txbas  15285  txcnp  15298  imasnopn  15326  ispsmet  15350  ismet  15371  isxmet  15372  ismet2  15381  blres  15461  metcnp3  15538  txmetcnp  15545  mulcncf  15635  ellimc3apf  15687  limcdifap  15689  limcmpted  15690  limccnp2lem  15703  dvmptfsum  15752  elply2  15762  sincosq3sgn  15855  pellexlem3  16010  lgsquadlem1  16113  2sqlem8  16159  2sqlem9  16160  eupthres  16615  eupth2lem3lem6fi  16629  subctctexmid  16947  nnnninfex  16973