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-mp 5  ax-1 6  ax-2 7  ax-3 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  2474  nonconne  2524  r2exf  2651  ceqsex3v  2898  ceqsex4v  2899  ceqsex8v  2901  reu2  3025  reu6  3026  reu4  3031  reu7  3032  2reu5lem3  3044  2reu5  3045  rmo3  3134  dfpss2  3355  difdif  3393  inass  3466  dfss4  3490  dfin2  3492  indi  3502  indifdir  3512  difin0ss  3617  inssdif0  3618  ssunpr  3869  dfpss4  3889  unipr  3906  uniun  3911  uniin  3912  iunin2  4031  iundif2  4034  iindif2  4036  iinin2  4037  elpw1  4145  eluni1g  4173  opkelimagekg  4272  xpkvexg  4286  sikexlem  4296  dfimak2  4299  dfpw12  4302  insklem  4305  addcass  4416  nnsucelr  4429  nndisjeq  4430  ltfinex  4465  ncfinraise  4482  nnpw1ex  4485  nnadjoin  4521  tfinnn  4535  eqvinop  4607  setconslem4  4735  fconstopab  4816  opeliunxp  4821  xpundi  4833  elcnv2  4891  cnvuni  4896  brres  4950  imai  5011  intasym  5029  imainss  5043  ssrnres  5060  cnvresima  5078  coundir  5084  rnco  5088  coass  5098  fncnv  5159  funcnvuni  5162  imadif  5172  iunfopab  5205  fint  5246  fin  5247  dff12  5258  f1funfun  5264  fores  5279  dff1o4  5295  f1ocnvb  5299  eqfnfv3  5395  unpreima  5409  inpreima  5410  ffnfvf  5429  fsn2  5435  funiunfv  5468  dff13f  5473  isocnv2  5493  isomin  5497  isoini  5498  dmsi  5520  ffnov  5588  eqfnov  5590  foov  5607  mptpreima  5683  dmmpt  5684  brsnsi2  5777  trtxp  5782  brtxp  5784  restxp  5787  oqelins4  5795  addcfnex  5825  brpprod  5840  fnfullfunlem1  5857  fvfullfunlem1  5862  fvfullfunlem3  5864  pmvalg  6011  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enprmaplem1  6077  enprmaplem4  6080  lecex  6116  ovmuc  6131  ce0nn  6181  nclennlem1  6249  addccan2nclem1  6264  nmembers1lem1  6269  nncdiv3lem1  6276  nnc3n3p1  6279  spacis  6289  nchoicelem16  6305  dmfrec  6317