Theorem anbi2i 675

Description: Introduce 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
bi.aa	|- (ph <-> ps)

Assertion

Ref	Expression
anbi2i	|- ((ch /\ ph) <-> (ch /\ ps))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 |- (ph <-> ps)
2	1	a1i 10	. 2 |- (ch -> (ph <-> ps))
3	2	pm5.32i 618	1 |- ((ch /\ ph) <-> (ch /\ ps))

Syntax hints:   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anbi12i  678  an4  797  an42  798  anandir  802  dfbi3  863  dn1  932  nannan  1291  cadan  1392  cadcoma  1395  nic-mpALT  1437  nic-axALT  1439  19.35  1600  19.27  1869  3exdistr  1910  4exdistr  1911  sb6  2099  2sb5  2112  2sb5rf  2117  sbel2x  2125  eu2  2229  eu3  2230  mo4f  2236  eu5  2242  eu4  2243  euan  2261  2mos  2283  2eu4  2287  2eu6  2289  clelab  2473  nonconne  2523  r2exf  2650  ceqsex3v  2897  ceqsex4v  2898  ceqsex8v  2900  reu2  3024  reu6  3025  reu4  3030  reu7  3031  2reu5lem3  3043  2reu5  3044  rmo3  3133  dfpss2  3354  difdif  3392  inass  3465  dfss4  3489  dfin2  3491  indi  3501  indifdir  3511  difin0ss  3616  inssdif0  3617  ssunpr  3868  dfpss4  3888  unipr  3905  uniun  3910  uniin  3911  iunin2  4030  iundif2  4033  iindif2  4035  iinin2  4036  elpw1  4144  eluni1g  4172  opkelimagekg  4271  xpkvexg  4285  sikexlem  4295  dfimak2  4298  dfpw12  4301  insklem  4304  addcass  4415  nnsucelr  4428  nndisjeq  4429  ltfinex  4464  ncfinraise  4481  nnpw1ex  4484  nnadjoin  4520  tfinnn  4534  eqvinop  4606  setconslem4  4734  fconstopab  4815  opeliunxp  4820  xpundi  4832  elcnv2  4890  cnvuni  4895  brres  4949  imai  5010  intasym  5028  imainss  5042  ssrnres  5059  cnvresima  5077  coundir  5083  rnco  5087  coass  5097  fncnv  5158  funcnvuni  5161  imadif  5171  iunfopab  5204  fint  5245  fin  5246  dff12  5257  f1funfun  5263  fores  5278  dff1o4  5294  f1ocnvb  5298  eqfnfv3  5394  unpreima  5408  inpreima  5409  ffnfvf  5428  fsn2  5434  funiunfv  5467  dff13f  5472  isocnv2  5492  isomin  5496  isoini  5497  dmsi  5519  ffnov  5587  eqfnov  5589  foov  5606  mptpreima  5682  dmmpt  5683  brsnsi2  5776  trtxp  5781  brtxp  5783  restxp  5786  oqelins4  5794  addcfnex  5824  brpprod  5839  fnfullfunlem1  5856  fvfullfunlem1  5861  fvfullfunlem3  5863  pmvalg  6010  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enprmaplem1  6076  enprmaplem4  6079  lecex  6115  ovmuc  6130  ce0nn  6180  nclennlem1  6248  addccan2nclem1  6263  nmembers1lem1  6268  nncdiv3lem1  6275  nnc3n3p1  6278  spacis  6288  nchoicelem16  6304  dmfrec  6316