Theorem anbi2d 464

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 450	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  467  anbi1cd  468  anbi12d  473  bi2anan9  606  dn1dc  960  xorbi2d  1380  dfbi3dc  1397  xordidc  1399  eleq2w  2239  eleq2  2241  ceqsex2  2777  ceqsex6v  2781  vtocl2gaf  2804  ceqsrex2v  2869  mob2  2917  eqreu  2929  nelrdva  2944  dfss4st  3368  undif4  3485  r19.27m  3518  ifbi  3554  preq12bg  3773  opeq2  3779  ralunsn  3797  intab  3873  disjiun  3998  brimralrspcev  4062  opabbid  4068  opthg  4238  pocl  4303  ordelord  4381  ordtriexmid  4520  ontr2exmid  4524  onsucsssucexmid  4526  tfisi  4586  xpeq2  4641  rabxp  4663  vtoclr  4674  opeliunxp  4681  posng  4698  opbrop  4705  rexiunxp  4769  elrnmpt1  4878  dfres2  4959  brcodir  5016  poltletr  5029  xp11m  5067  elxp4  5116  elxp5  5117  dffun4f  5232  fununi  5284  fneq2  5305  fnun  5322  feq3  5350  foeq3  5436  funfveu  5528  funbrfv  5554  ssimaexg  5578  fvopab3g  5589  fvopab3ig  5590  fvelrn  5647  fmptco  5682  fsn2  5690  elunirn  5766  isoeq2  5802  isoeq3  5803  isocnv2  5812  isoini  5818  isopolem  5822  f1oiso  5826  f1oiso2  5827  oprabbid  5927  cbvoprab3  5950  mpomptx  5965  mpofun  5976  ov  5993  ovi3  6010  ov6g  6011  ovg  6012  caoftrn  6107  f1o2ndf1  6228  xporderlem  6231  f1od2  6235  brtpos2  6251  brtposg  6254  dftpos4  6263  recseq  6306  tfrlem3-2d  6312  tfrlemi1  6332  tfrexlem  6334  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcl  6364  freceq1  6392  freceq2  6393  frecsuc  6407  nnaordex  6528  brecop  6624  eroveu  6625  erovlem  6626  ecopovtrn  6631  ecopovtrng  6634  th3qlem1  6636  th3qlem2  6637  th3q  6639  elpmg  6663  ixpsnval  6700  ixpsnf1o  6735  domeng  6751  dom2lem  6771  xpcomco  6825  xpassen  6829  xpdom2  6830  xpf1o  6843  phplem3g  6855  ssfiexmid  6875  domfiexmid  6877  findcard2  6888  findcard2s  6889  findcard2d  6890  findcard2sd  6891  diffifi  6893  fiintim  6927  fidcenumlemrk  6952  fidcenumlemr  6953  supeq2  6987  nnnninfeq2  7126  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  acfun  7205  2omotaplemap  7255  2omotaplemst  7256  exmidapne  7258  ccfunen  7262  recexnq  7388  recmulnqg  7389  ltsonq  7396  enq0sym  7430  enq0ref  7431  enq0tr  7432  enq0breq  7434  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  mulnnnq0  7448  elinp  7472  prdisj  7490  prarloclem3  7495  prarloc  7501  distrlem5prl  7584  distrlem5pru  7585  ltexprlemell  7596  ltexprlemelu  7597  recexprlemm  7622  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  lttrsr  7760  recexgt0sr  7771  mulgt0sr  7776  ltresr  7837  axprecex  7878  axpre-lttrn  7882  axpre-mulgt0  7885  eqlelt  8042  lesub0  8434  apreap  8542  apreim  8558  aprcl  8601  aptap  8605  zltlen  9329  prime  9350  fzind  9366  qltlen  9638  xltnegi  9833  ixxval  9894  fzval  10008  fzdifsuc  10078  elfzm11  10088  elfzo  10146  exbtwnzlemshrink  10246  rebtwn2zlemshrink  10251  facwordi  10715  zfz1iso  10816  shftfvalg  10822  shftfibg  10824  shftfval  10825  shftfib  10827  shftfn  10828  2shfti  10835  cau3lem  11118  caubnd2  11121  xrmaxiflemcom  11252  clim  11284  clim2  11286  climi  11290  climcn2  11312  addcn2  11313  subcn2  11314  mulcn2  11315  summodclem2a  11384  summodc  11386  fsum3  11390  fsumsplitf  11411  prodfdivap  11550  ntrivcvgap0  11552  prodeq1f  11555  prodeq2w  11559  prodeq2  11560  prodmodc  11581  zproddc  11582  fprodseq  11586  fprodntrivap  11587  fproddivapf  11634  fprodsplitf  11635  fprodsplit1f  11637  sinbnd  11755  cosbnd  11756  divalgb  11924  ndvdssub  11929  zsupcllemex  11941  gcdval  11954  gcdneg  11977  bezoutlemstep  11992  bezoutlemmain  11993  bezoutlemex  11996  dfgcd2  12009  gcdass  12010  algcvgblem  12043  lcmval  12057  lcmneg  12068  lcmgcdlem  12071  lcmass  12079  qredeq  12090  prmind2  12114  euclemma  12140  pw2dvdslemn  12159  qnumval  12179  qdenval  12180  pceu  12289  pczpre  12291  pcdiv  12296  prmpwdvds  12347  mnd1  12801  grp1  12930  nmznsg  13026  releqgg  13033  iscmnd  13054  issrg  13101  iscrng2  13151  opprunitd  13232  crngunit  13233  basis2  13439  eltg2  13446  isnei  13537  isneip  13539  restbasg  13561  iscnp  13592  iscnp3  13596  tgcn  13601  icnpimaex  13604  lmbrf  13608  cncnp  13623  cnptoprest2  13633  txbas  13651  txcnp  13664  imasnopn  13692  ispsmet  13716  ismet  13737  isxmet  13738  ismet2  13747  blres  13827  metcnp3  13904  txmetcnp  13911  mulcncf  13984  ellimc3apf  14022  limcdifap  14024  limcmpted  14025  limccnp2lem  14038  sincosq3sgn  14142  2sqlem8  14352  2sqlem9  14353  subctctexmid  14632