Theorem anbi2d 460

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 446	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  463  anbi12d  465  bi2anan9  596  dn1dc  950  xorbi2d  1370  dfbi3dc  1387  xordidc  1389  eleq2w  2227  eleq2  2229  ceqsex2  2765  ceqsex6v  2769  vtocl2gaf  2792  ceqsrex2v  2857  mob2  2905  eqreu  2917  nelrdva  2932  dfss4st  3354  undif4  3470  r19.27m  3503  ifbi  3539  preq12bg  3752  opeq2  3758  ralunsn  3776  intab  3852  disjiun  3976  brimralrspcev  4040  opabbid  4046  opthg  4215  pocl  4280  ordelord  4358  ordtriexmid  4497  ontr2exmid  4501  onsucsssucexmid  4503  tfisi  4563  xpeq2  4618  rabxp  4640  vtoclr  4651  opeliunxp  4658  posng  4675  opbrop  4682  rexiunxp  4745  elrnmpt1  4854  dfres2  4935  brcodir  4990  poltletr  5003  xp11m  5041  elxp4  5090  elxp5  5091  dffun4f  5203  fununi  5255  fneq2  5276  fnun  5293  feq3  5321  foeq3  5407  funfveu  5498  funbrfv  5524  ssimaexg  5547  fvopab3g  5558  fvopab3ig  5559  fvelrn  5615  fmptco  5650  fsn2  5658  elunirn  5733  isoeq2  5769  isoeq3  5770  isocnv2  5779  isoini  5785  isopolem  5789  f1oiso  5793  f1oiso2  5794  oprabbid  5891  cbvoprab3  5914  mpomptx  5929  mpofun  5940  ov  5957  ovi3  5974  ov6g  5975  ovg  5976  caoftrn  6074  f1o2ndf1  6192  xporderlem  6195  f1od2  6199  brtpos2  6215  brtposg  6218  dftpos4  6227  recseq  6270  tfrlem3-2d  6276  tfrlemi1  6296  tfrexlem  6298  tfr1onlemaccex  6312  tfrcllemaccex  6325  tfrcl  6328  freceq1  6356  freceq2  6357  frecsuc  6371  nnaordex  6491  brecop  6587  eroveu  6588  erovlem  6589  ecopovtrn  6594  ecopovtrng  6597  th3qlem1  6599  th3qlem2  6600  th3q  6602  elpmg  6626  ixpsnval  6663  ixpsnf1o  6698  domeng  6714  dom2lem  6734  xpcomco  6788  xpassen  6792  xpdom2  6793  xpf1o  6806  phplem3g  6818  ssfiexmid  6838  domfiexmid  6840  findcard2  6851  findcard2s  6852  findcard2d  6853  findcard2sd  6854  diffifi  6856  fiintim  6890  fidcenumlemrk  6915  fidcenumlemr  6916  supeq2  6950  nnnninfeq2  7089  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  acfun  7159  ccfunen  7201  recexnq  7327  recmulnqg  7328  ltsonq  7335  enq0sym  7369  enq0ref  7370  enq0tr  7371  enq0breq  7373  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  mulnnnq0  7387  elinp  7411  prdisj  7429  prarloclem3  7434  prarloc  7440  distrlem5prl  7523  distrlem5pru  7524  ltexprlemell  7535  ltexprlemelu  7536  recexprlemm  7561  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  lttrsr  7699  recexgt0sr  7710  mulgt0sr  7715  ltresr  7776  axprecex  7817  axpre-lttrn  7821  axpre-mulgt0  7824  eqlelt  7981  lesub0  8373  apreap  8481  apreim  8497  aprcl  8540  zltlen  9265  prime  9286  fzind  9302  qltlen  9574  xltnegi  9767  ixxval  9828  fzval  9942  fzdifsuc  10012  elfzm11  10022  elfzo  10080  exbtwnzlemshrink  10180  rebtwn2zlemshrink  10185  facwordi  10649  zfz1iso  10750  shftfvalg  10756  shftfibg  10758  shftfval  10759  shftfib  10761  shftfn  10762  2shfti  10769  cau3lem  11052  caubnd2  11055  xrmaxiflemcom  11186  clim  11218  clim2  11220  climi  11224  climcn2  11246  addcn2  11247  subcn2  11248  mulcn2  11249  summodclem2a  11318  summodc  11320  fsum3  11324  fsumsplitf  11345  prodfdivap  11484  ntrivcvgap0  11486  prodeq1f  11489  prodeq2w  11493  prodeq2  11494  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodntrivap  11521  fproddivapf  11568  fprodsplitf  11569  fprodsplit1f  11571  sinbnd  11689  cosbnd  11690  divalgb  11858  ndvdssub  11863  zsupcllemex  11875  gcdval  11888  gcdneg  11911  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemex  11930  dfgcd2  11943  gcdass  11944  algcvgblem  11977  lcmval  11991  lcmneg  12002  lcmgcdlem  12005  lcmass  12013  qredeq  12024  prmind2  12048  euclemma  12074  pw2dvdslemn  12093  qnumval  12113  qdenval  12114  pceu  12223  pczpre  12225  pcdiv  12230  prmpwdvds  12281  basis2  12646  eltg2  12653  isnei  12744  isneip  12746  restbasg  12768  iscnp  12799  iscnp3  12803  tgcn  12808  icnpimaex  12811  lmbrf  12815  cncnp  12830  cnptoprest2  12840  txbas  12858  txcnp  12871  imasnopn  12899  ispsmet  12923  ismet  12944  isxmet  12945  ismet2  12954  blres  13034  metcnp3  13111  txmetcnp  13118  mulcncf  13191  ellimc3apf  13229  limcdifap  13231  limcmpted  13232  limccnp2lem  13245  sincosq3sgn  13349  2sqlem8  13559  2sqlem9  13560  subctctexmid  13841