Theorem anbi2d 461

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 447	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  464  anbi1cd  465  anbi12d  470  bi2anan9  601  dn1dc  955  xorbi2d  1375  dfbi3dc  1392  xordidc  1394  eleq2w  2232  eleq2  2234  ceqsex2  2770  ceqsex6v  2774  vtocl2gaf  2797  ceqsrex2v  2862  mob2  2910  eqreu  2922  nelrdva  2937  dfss4st  3360  undif4  3477  r19.27m  3510  ifbi  3546  preq12bg  3760  opeq2  3766  ralunsn  3784  intab  3860  disjiun  3984  brimralrspcev  4048  opabbid  4054  opthg  4223  pocl  4288  ordelord  4366  ordtriexmid  4505  ontr2exmid  4509  onsucsssucexmid  4511  tfisi  4571  xpeq2  4626  rabxp  4648  vtoclr  4659  opeliunxp  4666  posng  4683  opbrop  4690  rexiunxp  4753  elrnmpt1  4862  dfres2  4943  brcodir  4998  poltletr  5011  xp11m  5049  elxp4  5098  elxp5  5099  dffun4f  5214  fununi  5266  fneq2  5287  fnun  5304  feq3  5332  foeq3  5418  funfveu  5509  funbrfv  5535  ssimaexg  5558  fvopab3g  5569  fvopab3ig  5570  fvelrn  5627  fmptco  5662  fsn2  5670  elunirn  5745  isoeq2  5781  isoeq3  5782  isocnv2  5791  isoini  5797  isopolem  5801  f1oiso  5805  f1oiso2  5806  oprabbid  5906  cbvoprab3  5929  mpomptx  5944  mpofun  5955  ov  5972  ovi3  5989  ov6g  5990  ovg  5991  caoftrn  6086  f1o2ndf1  6207  xporderlem  6210  f1od2  6214  brtpos2  6230  brtposg  6233  dftpos4  6242  recseq  6285  tfrlem3-2d  6291  tfrlemi1  6311  tfrexlem  6313  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfrcl  6343  freceq1  6371  freceq2  6372  frecsuc  6386  nnaordex  6507  brecop  6603  eroveu  6604  erovlem  6605  ecopovtrn  6610  ecopovtrng  6613  th3qlem1  6615  th3qlem2  6616  th3q  6618  elpmg  6642  ixpsnval  6679  ixpsnf1o  6714  domeng  6730  dom2lem  6750  xpcomco  6804  xpassen  6808  xpdom2  6809  xpf1o  6822  phplem3g  6834  ssfiexmid  6854  domfiexmid  6856  findcard2  6867  findcard2s  6868  findcard2d  6869  findcard2sd  6870  diffifi  6872  fiintim  6906  fidcenumlemrk  6931  fidcenumlemr  6932  supeq2  6966  nnnninfeq2  7105  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  acfun  7184  ccfunen  7226  recexnq  7352  recmulnqg  7353  ltsonq  7360  enq0sym  7394  enq0ref  7395  enq0tr  7396  enq0breq  7398  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  elinp  7436  prdisj  7454  prarloclem3  7459  prarloc  7465  distrlem5prl  7548  distrlem5pru  7549  ltexprlemell  7560  ltexprlemelu  7561  recexprlemm  7586  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  lttrsr  7724  recexgt0sr  7735  mulgt0sr  7740  ltresr  7801  axprecex  7842  axpre-lttrn  7846  axpre-mulgt0  7849  eqlelt  8006  lesub0  8398  apreap  8506  apreim  8522  aprcl  8565  zltlen  9290  prime  9311  fzind  9327  qltlen  9599  xltnegi  9792  ixxval  9853  fzval  9967  fzdifsuc  10037  elfzm11  10047  elfzo  10105  exbtwnzlemshrink  10205  rebtwn2zlemshrink  10210  facwordi  10674  zfz1iso  10776  shftfvalg  10782  shftfibg  10784  shftfval  10785  shftfib  10787  shftfn  10788  2shfti  10795  cau3lem  11078  caubnd2  11081  xrmaxiflemcom  11212  clim  11244  clim2  11246  climi  11250  climcn2  11272  addcn2  11273  subcn2  11274  mulcn2  11275  summodclem2a  11344  summodc  11346  fsum3  11350  fsumsplitf  11371  prodfdivap  11510  ntrivcvgap0  11512  prodeq1f  11515  prodeq2w  11519  prodeq2  11520  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodntrivap  11547  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  sinbnd  11715  cosbnd  11716  divalgb  11884  ndvdssub  11889  zsupcllemex  11901  gcdval  11914  gcdneg  11937  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemex  11956  dfgcd2  11969  gcdass  11970  algcvgblem  12003  lcmval  12017  lcmneg  12028  lcmgcdlem  12031  lcmass  12039  qredeq  12050  prmind2  12074  euclemma  12100  pw2dvdslemn  12119  qnumval  12139  qdenval  12140  pceu  12249  pczpre  12251  pcdiv  12256  prmpwdvds  12307  mnd1  12679  basis2  12840  eltg2  12847  isnei  12938  isneip  12940  restbasg  12962  iscnp  12993  iscnp3  12997  tgcn  13002  icnpimaex  13005  lmbrf  13009  cncnp  13024  cnptoprest2  13034  txbas  13052  txcnp  13065  imasnopn  13093  ispsmet  13117  ismet  13138  isxmet  13139  ismet2  13148  blres  13228  metcnp3  13305  txmetcnp  13312  mulcncf  13385  ellimc3apf  13423  limcdifap  13425  limcmpted  13426  limccnp2lem  13439  sincosq3sgn  13543  2sqlem8  13753  2sqlem9  13754  subctctexmid  14034