Theorem anbi1d 469

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi1  470  anbi12d  477  bi2anan9  614  pm5.71dc  974  dfifp4dc  996  dfifp5dc  997  xorbi1d  1430  drsb1  1852  ax11ev  1881  eleq1w  2299  eleq1  2301  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  vtocl2gaf  2890  alexeq  2952  ceqex  2953  elrabi  2979  sbc5  3075  rexss  3315  ineq1  3425  difin2  3493  r19.28m  3617  elif  3652  ifeqeqxdc  3687  rabsnifsb  3777  preq12bg  3898  opeq1  3904  eluni  3938  disjiun  4125  mpteq12f  4211  axsepg  4250  sepg  4251  zfausclOLD  4253  opthg  4378  copsexg  4384  euotd  4395  elopab  4400  pocl  4448  uniuni  4597  rabxfrd  4615  ontr2exmid  4672  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  preleq  4702  xpeq1  4788  elxpi  4790  vtoclr  4823  opbrop  4854  opelresg  5070  resopab2  5110  elxp4  5275  elxp5  5276  cnvpom  5330  fun11  5448  feq2  5517  f1eq2  5594  f1eq3  5595  foeq2  5612  brprcneu  5688  ssimaexg  5765  dmfco  5773  fndmdif  5814  respreima  5836  isoeq5  6011  isoini  6024  isopolem  6028  f1oiso  6032  f1oiso2  6033  riotaeqdv  6039  acexmidlemab  6079  acexmidlemcase  6080  oprabid  6117  mpoeq123  6147  mpoeq123dva  6149  eloprabga  6175  resoprab  6184  resoprab2  6185  ov  6208  ovi3  6226  ov6g  6227  ovg  6228  caoftrn  6335  opabex3d  6350  opabex3  6351  elxp7  6404  eloprabi  6432  cnvf1o  6461  xporderlem  6467  poxp  6468  rexsupp  6493  smoel2  6574  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnaordex  6801  qliftel  6889  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  th3q  6914  ixpsnf1o  7018  dom2lem  7058  mapsnend  7099  modom  7108  xpsnen  7119  xpassen  7128  pw2f1odclem  7134  xpf1o  7144  opabfi  7247  ctssdccl  7451  exmidapne  7626  dfplpq2  7721  dfmpq2  7722  ltsonq  7765  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  elinp  7841  prnmaxl  7855  prnminu  7856  prarloclemlo  7861  prarloc  7870  genpdflem  7874  genpassl  7891  genpassu  7892  ltexprlemm  7967  recexprlemell  7989  recexprlemelu  7990  cauappcvgprlemdisj  8018  caucvgprlemnkj  8033  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  lttrsr  8129  mulgt0sr  8145  ltresr  8206  axpre-lttrn  8251  axpre-mulgt0  8254  recexgt0  8908  apreap  8915  apreim  8931  aprcl  8974  aptap  8978  prime  9745  rexuz  9980  ltxr  10177  ixxval  10298  fzval  10413  hashfibclem  11282  hashf1lem2  11286  eqwrd  11345  pfxeq  11468  wrd2ind  11495  sqrtrval  11766  abslt  11854  absle  11855  lenegsq  11861  abs2difabs  11874  2clim  12067  climcn2  12075  addcn2  12076  mulcn2  12078  climrecvg1n  12114  sumeq1  12121  fsum2dlemstep  12201  modfsummod  12225  prodeq1f  12319  fprod2dlemstep  12389  nndivdvds  12563  divalg2  12693  gcdval  12736  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemex  12778  gcdass  12792  lcmval  12841  lcmass  12863  rpexp  12931  pythagtriplem2  13045  pythagtrip  13062  gzsumfzval  13711  issgrpv  13719  issgrpn0  13720  ismhm  13768  mhmpropd  13773  issubm  13779  issubg  13976  issubg3  13995  ringpropd  14343  crngpropd  14344  opprunitd  14417  issubrg  14529  resrhm2b  14557  islmod  14627  lmodlema  14628  lmodprop2d  14685  islssm  14694  islssmg  14695  lsslss  14718  znleval  14988  psrbag  15053  istopg  15100  basis2  15149  tg2  15161  iscld  15204  neival  15244  isnei  15245  isneip  15247  iscn  15298  cnpval  15299  iscnp  15300  txbas  15359  txdis1cn  15379  ispsmet  15424  ismet  15445  isxmet  15446  ismet2  15455  blres  15535  elmopn  15547  mopni  15583  neibl  15592  metrest  15607  elcncf  15674  mulc1cncf  15690  mulcncf  15709  limccnp2lem  15777  sincosq2sgn  15928  sincosq4sgn  15930  pellexlem3  16093  2lgslem1a  16207  edgssv2en  16440  uhgr2edg  16447  vtxdfifiun  16538  trlsfvalg  16624  istrl  16626  clwwlknp  16658  iseupth  16688  eupth2lem2dc  16700  bdsep2  16912  bdsepg  16916  bj-d0clsepcl  16951  sscoll2  17014  wexmiddifxy  17046