Theorem anbi1d 465

Description: Deduction adding a right 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
anbi1d	|- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Proof of Theorem anbi1d

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

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:  anbi1  466  anbi12d  473  bi2anan9  610  pm5.71dc  969  dfifp4dc  991  dfifp5dc  992  xorbi1d  1425  drsb1  1847  ax11ev  1876  eleq1w  2292  eleq1  2294  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  rabeqf  2792  vtocl2gaf  2871  alexeq  2932  ceqex  2933  elrabi  2959  sbc5  3055  rexss  3294  ineq1  3401  difin2  3469  r19.28m  3584  elif  3617  rabsnifsb  3737  preq12bg  3856  opeq1  3862  eluni  3896  disjiun  4083  mpteq12f  4169  axsep2  4208  zfauscl  4209  opthg  4330  copsexg  4336  euotd  4347  elopab  4352  pocl  4400  uniuni  4548  rabxfrd  4566  ontr2exmid  4623  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  preleq  4653  xpeq1  4739  elxpi  4741  vtoclr  4774  opbrop  4805  opelresg  5020  resopab2  5060  elxp4  5224  elxp5  5225  cnvpom  5279  fun11  5397  feq2  5466  f1eq2  5538  f1eq3  5539  foeq2  5556  brprcneu  5632  ssimaexg  5708  dmfco  5714  fndmdif  5752  rexsupp  5771  respreima  5775  isoeq5  5946  isoini  5959  isopolem  5963  f1oiso  5967  f1oiso2  5968  riotaeqdv  5972  acexmidlemab  6012  acexmidlemcase  6013  oprabid  6050  mpoeq123  6080  mpoeq123dva  6082  eloprabga  6108  resoprab  6117  resoprab2  6118  ov  6141  ovi3  6159  ov6g  6160  ovg  6161  caoftrn  6268  opabex3d  6283  opabex3  6284  elxp7  6333  eloprabi  6361  cnvf1o  6390  xporderlem  6396  poxp  6397  smoel2  6469  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnaordex  6696  qliftel  6784  brecop  6794  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem2  6807  th3q  6809  ixpsnf1o  6905  dom2lem  6945  modom  6994  xpsnen  7005  xpassen  7014  pw2f1odclem  7020  xpf1o  7030  opabfi  7132  ctssdccl  7310  exmidapne  7479  dfplpq2  7574  dfmpq2  7575  ltsonq  7618  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  elinp  7694  prnmaxl  7708  prnminu  7709  prarloclemlo  7714  prarloc  7723  genpdflem  7727  genpassl  7744  genpassu  7745  ltexprlemm  7820  recexprlemell  7842  recexprlemelu  7843  cauappcvgprlemdisj  7871  caucvgprlemnkj  7886  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  lttrsr  7982  mulgt0sr  7998  ltresr  8059  axpre-lttrn  8104  axpre-mulgt0  8107  recexgt0  8760  apreap  8767  apreim  8783  aprcl  8826  aptap  8830  prime  9579  rexuz  9814  ltxr  10010  ixxval  10131  fzval  10245  eqwrd  11158  pfxeq  11281  wrd2ind  11308  sqrtrval  11578  abslt  11666  absle  11667  lenegsq  11673  abs2difabs  11686  2clim  11879  climcn2  11887  addcn2  11888  mulcn2  11890  climrecvg1n  11926  sumeq1  11933  fsum2dlemstep  12013  modfsummod  12037  prodeq1f  12131  fprod2dlemstep  12201  nndivdvds  12375  divalg2  12505  gcdval  12548  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemex  12590  gcdass  12604  lcmval  12653  lcmass  12675  rpexp  12743  pythagtriplem2  12857  pythagtrip  12874  gsumfzval  13492  issgrpv  13505  issgrpn0  13506  ismhm  13562  mhmpropd  13567  issubm  13573  issubg  13778  issubg3  13797  ringpropd  14070  crngpropd  14071  opprunitd  14143  issubrg  14254  resrhm2b  14282  islmod  14324  lmodlema  14325  lmodprop2d  14381  islssm  14390  islssmg  14391  lsslss  14414  znleval  14686  psrbag  14702  istopg  14742  basis2  14791  tg2  14803  iscld  14846  neival  14886  isnei  14887  isneip  14889  iscn  14940  cnpval  14941  iscnp  14942  txbas  15001  txdis1cn  15021  ispsmet  15066  ismet  15087  isxmet  15088  ismet2  15097  blres  15177  elmopn  15189  mopni  15225  neibl  15234  metrest  15249  elcncf  15316  mulc1cncf  15332  mulcncf  15351  limccnp2lem  15419  sincosq2sgn  15570  sincosq4sgn  15572  2lgslem1a  15836  edgssv2en  16069  uhgr2edg  16076  vtxdfifiun  16167  trlsfvalg  16253  istrl  16255  clwwlknp  16287  iseupth  16317  eupth2lem2dc  16329  bdsep2  16532  bdzfauscl  16536  bj-d0clsepcl  16571  sscoll2  16634