Theorem anbi2d 460

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 446	1 |- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

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  463  anbi12d  465  bi2anan9  596  dn1dc  945  xorbi2d  1359  dfbi3dc  1376  xordidc  1378  eleq2w  2202  eleq2  2204  ceqsex2  2729  ceqsex6v  2733  vtocl2gaf  2756  ceqsrex2v  2821  mob2  2868  eqreu  2880  nelrdva  2895  dfss4st  3314  undif4  3430  r19.27m  3463  ifbi  3497  preq12bg  3708  opeq2  3714  ralunsn  3732  intab  3808  disjiun  3932  brimralrspcev  3995  opabbid  4001  opthg  4168  pocl  4233  ordelord  4311  ordtriexmid  4445  ontr2exmid  4448  onsucsssucexmid  4450  tfisi  4509  xpeq2  4562  rabxp  4584  vtoclr  4595  opeliunxp  4602  posng  4619  opbrop  4626  rexiunxp  4689  elrnmpt1  4798  dfres2  4879  brcodir  4934  poltletr  4947  xp11m  4985  elxp4  5034  elxp5  5035  dffun4f  5147  fununi  5199  fneq2  5220  fnun  5237  feq3  5265  foeq3  5351  funfveu  5442  funbrfv  5468  ssimaexg  5491  fvopab3g  5502  fvopab3ig  5503  fvelrn  5559  fmptco  5594  fsn2  5602  elunirn  5675  isoeq2  5711  isoeq3  5712  isocnv2  5721  isoini  5727  isopolem  5731  f1oiso  5735  f1oiso2  5736  oprabbid  5832  cbvoprab3  5855  mpomptx  5870  mpofun  5881  ov  5898  ovi3  5915  ov6g  5916  ovg  5917  caoftrn  6015  f1o2ndf1  6133  xporderlem  6136  f1od2  6140  brtpos2  6156  brtposg  6159  dftpos4  6168  recseq  6211  tfrlem3-2d  6217  tfrlemi1  6237  tfrexlem  6239  tfr1onlemaccex  6253  tfrcllemaccex  6266  tfrcl  6269  freceq1  6297  freceq2  6298  frecsuc  6312  nnaordex  6431  brecop  6527  eroveu  6528  erovlem  6529  ecopovtrn  6534  ecopovtrng  6537  th3qlem1  6539  th3qlem2  6540  th3q  6542  elpmg  6566  ixpsnval  6603  ixpsnf1o  6638  domeng  6654  dom2lem  6674  xpcomco  6728  xpassen  6732  xpdom2  6733  xpf1o  6746  phplem3g  6758  ssfiexmid  6778  domfiexmid  6780  findcard2  6791  findcard2s  6792  findcard2d  6793  findcard2sd  6794  diffifi  6796  fiintim  6825  fidcenumlemrk  6850  fidcenumlemr  6851  supeq2  6884  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  ccfunen  7096  recexnq  7222  recmulnqg  7223  ltsonq  7230  enq0sym  7264  enq0ref  7265  enq0tr  7266  enq0breq  7268  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  mulnnnq0  7282  elinp  7306  prdisj  7324  prarloclem3  7329  prarloc  7335  distrlem5prl  7418  distrlem5pru  7419  ltexprlemell  7430  ltexprlemelu  7431  recexprlemm  7456  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  lttrsr  7594  recexgt0sr  7605  mulgt0sr  7610  ltresr  7671  axprecex  7712  axpre-lttrn  7716  axpre-mulgt0  7719  lesub0  8265  apreap  8373  apreim  8389  aprcl  8432  zltlen  9153  prime  9174  fzind  9190  qltlen  9459  xltnegi  9648  ixxval  9709  fzval  9823  fzdifsuc  9892  elfzm11  9902  elfzo  9957  exbtwnzlemshrink  10057  rebtwn2zlemshrink  10062  facwordi  10518  zfz1iso  10616  shftfvalg  10622  shftfibg  10624  shftfval  10625  shftfib  10627  shftfn  10628  2shfti  10635  cau3lem  10918  caubnd2  10921  xrmaxiflemcom  11050  clim  11082  clim2  11084  climi  11088  climcn2  11110  addcn2  11111  subcn2  11112  mulcn2  11113  summodclem2a  11182  summodc  11184  fsum3  11188  fsumsplitf  11209  prodfdivap  11348  ntrivcvgap0  11350  prodeq1f  11353  prodeq2w  11357  prodeq2  11358  prodmodc  11379  zproddc  11380  fprodseq  11384  sinbnd  11495  cosbnd  11496  divalgb  11658  ndvdssub  11663  zsupcllemex  11675  gcdval  11684  gcdneg  11706  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemex  11725  dfgcd2  11738  gcdass  11739  algcvgblem  11766  lcmval  11780  lcmneg  11791  lcmgcdlem  11794  lcmass  11802  qredeq  11813  prmind2  11837  euclemma  11860  pw2dvdslemn  11879  qnumval  11899  qdenval  11900  basis2  12254  eltg2  12261  isnei  12352  isneip  12354  restbasg  12376  iscnp  12407  iscnp3  12411  tgcn  12416  icnpimaex  12419  lmbrf  12423  cncnp  12438  cnptoprest2  12448  txbas  12466  txcnp  12479  imasnopn  12507  ispsmet  12531  ismet  12552  isxmet  12553  ismet2  12562  blres  12642  metcnp3  12719  txmetcnp  12726  mulcncf  12799  ellimc3apf  12837  limcdifap  12839  limcmpted  12840  limccnp2lem  12853  sincosq3sgn  12957  subctctexmid  13369