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  606  pm5.71dc  964  xorbi1d  1401  drsb1  1822  ax11ev  1851  eleq1w  2266  eleq1  2268  rexeqf  2699  reueq1f  2700  rmoeq1f  2701  rabeqf  2762  vtocl2gaf  2840  alexeq  2899  ceqex  2900  elrabi  2926  sbc5  3022  rexss  3260  ineq1  3367  difin2  3435  r19.28m  3550  preq12bg  3814  opeq1  3819  eluni  3853  disjiun  4039  mpteq12f  4124  axsep2  4163  zfauscl  4164  opthg  4282  copsexg  4288  euotd  4299  elopab  4304  pocl  4350  uniuni  4498  rabxfrd  4516  ontr2exmid  4573  regexmidlemm  4580  regexmidlem1  4581  reg2exmidlema  4582  preleq  4603  xpeq1  4689  elxpi  4691  vtoclr  4723  opbrop  4754  opelresg  4966  resopab2  5006  elxp4  5170  elxp5  5171  cnvpom  5225  fun11  5341  feq2  5409  f1eq2  5477  f1eq3  5478  foeq2  5495  brprcneu  5569  ssimaexg  5641  dmfco  5647  fndmdif  5685  rexsupp  5704  respreima  5708  isoeq5  5874  isoini  5887  isopolem  5891  f1oiso  5895  f1oiso2  5896  riotaeqdv  5900  acexmidlemab  5938  acexmidlemcase  5939  oprabid  5976  mpoeq123  6004  mpoeq123dva  6006  eloprabga  6032  resoprab  6041  resoprab2  6042  ov  6065  ovi3  6083  ov6g  6084  ovg  6085  caoftrn  6191  opabex3d  6206  opabex3  6207  elxp7  6256  eloprabi  6282  cnvf1o  6311  xporderlem  6317  poxp  6318  smoel2  6389  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  nnaordex  6614  qliftel  6702  brecop  6712  eroveu  6713  ecopovtrn  6719  ecopovtrng  6722  th3qlem2  6725  th3q  6727  ixpsnf1o  6823  dom2lem  6863  xpsnen  6916  xpassen  6925  pw2f1odclem  6931  xpf1o  6941  opabfi  7035  ctssdccl  7213  exmidapne  7372  dfplpq2  7467  dfmpq2  7468  ltsonq  7511  enq0sym  7545  enq0ref  7546  enq0tr  7547  enq0breq  7549  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  mulnnnq0  7563  elinp  7587  prnmaxl  7601  prnminu  7602  prarloclemlo  7607  prarloc  7616  genpdflem  7620  genpassl  7637  genpassu  7638  ltexprlemm  7713  recexprlemell  7735  recexprlemelu  7736  cauappcvgprlemdisj  7764  caucvgprlemnkj  7779  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  lttrsr  7875  mulgt0sr  7891  ltresr  7952  axpre-lttrn  7997  axpre-mulgt0  8000  recexgt0  8653  apreap  8660  apreim  8676  aprcl  8719  aptap  8723  prime  9472  rexuz  9701  ltxr  9897  ixxval  10018  fzval  10132  eqwrd  11034  sqrtrval  11311  abslt  11399  absle  11400  lenegsq  11406  abs2difabs  11419  2clim  11612  climcn2  11620  addcn2  11621  mulcn2  11623  climrecvg1n  11659  sumeq1  11666  fsum2dlemstep  11745  modfsummod  11769  prodeq1f  11863  fprod2dlemstep  11933  nndivdvds  12107  divalg2  12237  gcdval  12280  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemex  12322  gcdass  12336  lcmval  12385  lcmass  12407  rpexp  12475  pythagtriplem2  12589  pythagtrip  12606  gsumfzval  13223  issgrpv  13236  issgrpn0  13237  ismhm  13293  mhmpropd  13298  issubm  13304  issubg  13509  issubg3  13528  ringpropd  13800  crngpropd  13801  opprunitd  13872  issubrg  13983  resrhm2b  14011  islmod  14053  lmodlema  14054  lmodprop2d  14110  islssm  14119  islssmg  14120  lsslss  14143  znleval  14415  psrbag  14431  istopg  14471  basis2  14520  tg2  14532  iscld  14575  neival  14615  isnei  14616  isneip  14618  iscn  14669  cnpval  14670  iscnp  14671  txbas  14730  txdis1cn  14750  ispsmet  14795  ismet  14816  isxmet  14817  ismet2  14826  blres  14906  elmopn  14918  mopni  14954  neibl  14963  metrest  14978  elcncf  15045  mulc1cncf  15061  mulcncf  15080  limccnp2lem  15148  sincosq2sgn  15299  sincosq4sgn  15301  2lgslem1a  15565  bdsep2  15822  bdzfauscl  15826  bj-d0clsepcl  15861  sscoll2  15924