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  5945  isoini  5958  isopolem  5962  f1oiso  5966  f1oiso2  5967  riotaeqdv  5971  acexmidlemab  6011  acexmidlemcase  6012  oprabid  6049  mpoeq123  6079  mpoeq123dva  6081  eloprabga  6107  resoprab  6116  resoprab2  6117  ov  6140  ovi3  6158  ov6g  6159  ovg  6160  caoftrn  6267  opabex3d  6282  opabex3  6283  elxp7  6332  eloprabi  6360  cnvf1o  6389  xporderlem  6395  poxp  6396  smoel2  6468  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  nnaordex  6695  qliftel  6783  brecop  6793  eroveu  6794  ecopovtrn  6800  ecopovtrng  6803  th3qlem2  6806  th3q  6808  ixpsnf1o  6904  dom2lem  6944  modom  6993  xpsnen  7004  xpassen  7013  pw2f1odclem  7019  xpf1o  7029  opabfi  7131  ctssdccl  7309  exmidapne  7478  dfplpq2  7573  dfmpq2  7574  ltsonq  7617  enq0sym  7651  enq0ref  7652  enq0tr  7653  enq0breq  7655  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  elinp  7693  prnmaxl  7707  prnminu  7708  prarloclemlo  7713  prarloc  7722  genpdflem  7726  genpassl  7743  genpassu  7744  ltexprlemm  7819  recexprlemell  7841  recexprlemelu  7842  cauappcvgprlemdisj  7870  caucvgprlemnkj  7885  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  lttrsr  7981  mulgt0sr  7997  ltresr  8058  axpre-lttrn  8103  axpre-mulgt0  8106  recexgt0  8759  apreap  8766  apreim  8782  aprcl  8825  aptap  8829  prime  9578  rexuz  9813  ltxr  10009  ixxval  10130  fzval  10244  eqwrd  11153  pfxeq  11276  wrd2ind  11303  sqrtrval  11560  abslt  11648  absle  11649  lenegsq  11655  abs2difabs  11668  2clim  11861  climcn2  11869  addcn2  11870  mulcn2  11872  climrecvg1n  11908  sumeq1  11915  fsum2dlemstep  11994  modfsummod  12018  prodeq1f  12112  fprod2dlemstep  12182  nndivdvds  12356  divalg2  12486  gcdval  12529  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemex  12571  gcdass  12585  lcmval  12634  lcmass  12656  rpexp  12724  pythagtriplem2  12838  pythagtrip  12855  gsumfzval  13473  issgrpv  13486  issgrpn0  13487  ismhm  13543  mhmpropd  13548  issubm  13554  issubg  13759  issubg3  13778  ringpropd  14050  crngpropd  14051  opprunitd  14123  issubrg  14234  resrhm2b  14262  islmod  14304  lmodlema  14305  lmodprop2d  14361  islssm  14370  islssmg  14371  lsslss  14394  znleval  14666  psrbag  14682  istopg  14722  basis2  14771  tg2  14783  iscld  14826  neival  14866  isnei  14867  isneip  14869  iscn  14920  cnpval  14921  iscnp  14922  txbas  14981  txdis1cn  15001  ispsmet  15046  ismet  15067  isxmet  15068  ismet2  15077  blres  15157  elmopn  15169  mopni  15205  neibl  15214  metrest  15229  elcncf  15296  mulc1cncf  15312  mulcncf  15331  limccnp2lem  15399  sincosq2sgn  15550  sincosq4sgn  15552  2lgslem1a  15816  edgssv2en  16049  uhgr2edg  16056  vtxdfifiun  16147  trlsfvalg  16233  istrl  16235  clwwlknp  16267  iseupth  16297  eupth2lem2dc  16309  bdsep2  16481  bdzfauscl  16485  bj-d0clsepcl  16520  sscoll2  16583