Theorem anbi2i 730

Description: Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbi.1	|- ( ph <-> ps )

Assertion

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

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 |- ( ph <-> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.32i 669	1 |- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

Syntax hints:   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  anbi12i  733  bianass  842  an4  865  an42  866  anandir  872  dfbi3  994  dfbi3OLD  995  dn1  1008  dfifp3  1015  an3andi  1445  an33rean  1446  anxordi  1479  cadcoma  1551  nic-mpALT  1597  nic-axALT  1599  19.27v  1908  19.41v  1914  3exdistr  1923  4exdistr  1924  19.27  2095  19.41  2103  19.27OLD  2234  sbn  2391  2sb5  2443  eu5  2496  eu3v  2498  eu2  2509  mo4f  2516  eu4  2518  2mos  2552  2eu4  2556  rexbii  3041  ceqsex3v  3246  ceqsex4v  3247  ceqsex8v  3249  reu2  3394  reu6  3395  reu4  3400  reu7  3401  2reu5lem3  3415  2reu5  3416  rmo3  3528  dfpss2  3692  difdif  3736  raldifb  3750  inass  3823  dfss4  3858  dfin2  3860  indi  3873  indifdir  3883  undif3  3888  difin0ss  3946  inssdif0  3947  rexdifpr  4205  ssunpr  4365  unipr  4449  uniun  4456  uniin  4457  csbuni  4466  iunin2  4584  iundif2  4587  iindif2  4589  iinin2  4590  elpwpw  4613  axrep1  4772  axrep4  4775  notzfaus  4840  reusv2lem4  4872  eqvinop  4955  opcom  4965  opeqsn  4967  snopeqop  4969  fconstmpt  5163  opeliunxp  5170  xpundi  5171  elvvv  5178  xpiindi  5257  elcnv2  5300  cnvuni  5309  dmuni  5334  opelres  5401  elima3  5473  imai  5478  imainss  5548  difxp  5558  xpdifid  5562  ssrnres  5572  mptpreima  5628  coundir  5637  rnco  5641  coass  5654  relrelss  5659  wfi  5713  ordtri3or  5755  dffun2  5898  dffun3  5899  dffun4  5900  dffun5  5901  dffun6f  5902  dffun7  5915  dffun8  5916  dffun9  5917  svrelfun  5961  fncnv  5962  imadif  5973  dfmpt3  6014  fint  6084  fin  6085  dff12  6100  fores  6124  dff1o4  6145  eqfnfv3  6313  fndmin  6324  fniniseg  6338  unpreima  6341  ffnfvf  6389  fsn2  6403  tpres  6466  fconstfv  6476  dff13f  6513  dff14a  6527  dff14b  6528  isocnv2  6581  ffnov  6764  eqfnov  6766  foov  6808  uniuni  6971  tfindsg  7060  findsg  7093  funcnvuni  7119  opabex3d  7145  opabex3  7146  frxp  7287  soxp  7290  suppvalbr  7299  mpt2xopovel  7346  brtpos  7361  tpostpos  7372  dfsmo2  7444  dfrecs3  7469  rdglem1  7511  tz7.49  7540  brwitnlem  7587  oeeu  7683  erinxp  7821  mapsncnv  7904  cbvixp  7925  ixpin  7933  ixpiin  7934  mptelixpg  7945  elixpsn  7947  ixpsnf1o  7948  mapsnen  8035  xpassen  8054  omxpenlem  8061  sbthcl  8082  wemapsolem  8455  dford2  8517  inf2  8520  zfinf  8536  trcl  8604  iscard2  8802  leweon  8834  aceq1  8940  dfac3  8944  dfac4  8945  dfac5lem2  8947  dfac5lem3  8948  dfac5  8951  kmlem3  8974  kmlem4  8975  kmlem14  8985  kmlem15  8986  dfackm  8988  infmap2  9040  cf0  9073  fin23lem25  9146  zorn2lem7  9324  brdom6disj  9354  zfcndrep  9436  zfcndinf  9440  fpwwe  9468  axgroth4  9654  grothprim  9656  grothtsk  9657  nqpr  9836  addsrmo  9894  mulsrmo  9895  opelreal  9951  elnnz  11387  elznn0nn  11391  peano2uz2  11465  nnwos  11755  dflt2  11981  xmullem  12094  elfzuzb  12336  4fvwrd4  12459  preduz  12461  elfznelfzo  12573  fzind2  12586  fsuppmapnn0fiubex  12792  hashinfxadd  13174  hashfun  13224  fi1uzind  13279  brfi1uzind  13280  opfi1uzind  13283  fi1uzindOLD  13285  brfi1uzindOLD  13286  opfi1uzindOLD  13289  cotr2g  13715  shftdm  13811  rexfiuz  14087  cbvsum  14425  mertenslem2  14617  mertens  14618  cbvprod  14645  prodmo  14666  iprodmul  14734  divalglem10  15125  ndvdssub  15133  bitsmod  15158  algcvgblem  15290  isprm2  15395  isprm4  15397  hashdvds  15480  infpn2  15617  hashbc0  15709  xpscf  16226  funcpropd  16560  isffth2  16576  eldmcoa  16715  setcinv  16740  xpccatid  16828  yonedainv  16921  ispos  16947  ispos2  16948  joinfval2  17002  meetfval2  17016  istsr2  17218  isnsg2  17624  isnsg4  17637  isgim  17704  oppgid  17786  oppgcntz  17794  symgfix2  17836  efgval2  18137  iscyg2  18284  dmdprdd  18398  subgdmdprd  18433  issrg  18507  oppr1  18634  opprunit  18661  opprirred  18702  isrhm  18721  subsubrg2  18807  islmim  19062  lbsextg  19162  lidlnz  19228  isdomn2  19299  opsrtoslem1  19484  resubdrg  19954  unocv  20024  pjfval2  20053  islinds2  20152  mdetunilem8  20425  fvmptnn04if  20654  istop2g  20701  isbasis2g  20752  tgval2  20760  isclo2  20892  isnrm2  21162  is1stc2  21245  llyi  21277  isfbas2  21639  elfg  21675  ufinffr  21733  isfcls  21813  alexsubALTlem2  21852  alexsubALTlem3  21853  cnextcn  21871  ustfilxp  22016  iscusp2  22106  elcncf1di  22698  isclmp  22897  iscvsp  22928  tchcph  23036  iscau3  23076  caucfil  23081  ellogdm  24385  dvdsflsumcom  24914  logfac2  24942  dchrelbas3  24963  dchrvmasumlema  25189  legtrid  25486  outpasch  25647  axcontlem5  25848  axcontlem6  25849  axcontlem7  25850  nb3grpr2  26285  pthdlem1  26662  wwlksnextinj  26794  usgr2wspthon  26858  rusgrnumwwlkl1  26863  isclwwlks  26880  iseupthf1o  27062  frcond3  27133  frgr3v  27139  4cycl2vnunb  27154  frgrncvvdeqlem2  27164  fusgr2wsp2nb  27198  numclwwlkovf2  27217  numclwwlk3lem  27241  hhcms  28060  isch3  28098  ocsh  28142  pjhtheu  28253  pjpreeq  28257  h1deoi  28408  h1dei  28409  eleigvec  28816  cvbr2  29142  cvnbtwn2  29146  cvnbtwn4  29148  mdsl2i  29181  cvmdi  29183  mdsymlem6  29267  cdj3lem3b  29299  mo5f  29324  nmo  29325  rexunirn  29331  rmo3f  29335  rmo4fOLD  29336  rmo4f  29337  difrab2  29339  disjunsn  29407  unipreima  29446  dfcnv2  29476  1stpreima  29484  isrnsigaOLD  30175  isrnsiga  30176  rossros  30243  omsmeas  30385  eulerpartlemr  30436  eulerpartlemgvv  30438  ballotlemodife  30559  plymulx  30625  signstfvneq0  30649  bnj251  30768  bnj252  30769  bnj257  30773  bnj290  30776  bnj1304  30890  bnj153  30950  bnj543  30963  bnj571  30976  bnj580  30983  bnj607  30986  bnj882  30996  bnj964  31013  bnj996  31025  bnj1033  31037  bnj1176  31073  bnj1186  31075  bnj1189  31077  bnj1204  31080  bnj1253  31085  bnj1452  31120  bnj1463  31123  erdszelem9  31181  cvmlift2lem9  31293  cvmlift2lem13  31297  elmthm  31473  axinfprim  31583  axacprim  31584  coep  31641  dfso2  31644  fv1stcnv  31680  fv2ndcnv  31681  dford5reg  31687  dfon2lem5  31692  dfon2  31697  trpredmintr  31731  frind  31740  frr3g  31779  nosupno  31849  dmscut  31918  brtxp2  31988  brpprod3a  31993  dfom5b  32019  brcart  32039  brimg  32044  funpartlem  32049  dfrecs2  32057  cgrxfr  32162  segletr  32221  trer  32310  fneval  32347  neifg  32366  df3nandALT1  32396  andnand1  32398  nandsym1  32421  bj-dfssb2  32640  bj-axrep1  32788  bj-axrep4  32791  bj-eu3f  32829  bj-cleljustab  32847  bj-csbsnlem  32898  bj-snsetex  32951  bj-elsngl  32956  bj-snglc  32957  bj-restuni  33050  bj-ismooredr2  33065  bj-dfmpt2a  33071  mptsnunlem  33185  icorempt2  33199  isbasisrelowllem2  33204  relowlpssretop  33212  rdgeqoa  33218  dffinxpf  33222  curf  33387  finixpnum  33394  ptrest  33408  poimirlem1  33410  poimirlem14  33423  poimirlem16  33425  poimirlem19  33428  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimir  33442  cnambfre  33458  itg2addnc  33464  ftc1anc  33493  opropabco  33518  f1opr  33519  isdrngo1  33755  keridl  33831  ispridlc  33869  selconj  33902  anbi1ci  33996  brresALTV  34032  eldmqsres  34051  cnvepres  34066  opelinxp  34111  ecinn0  34118  alrmomo  34123  motr  34127  prtlem70  34141  prtlem100  34144  prtlem15  34160  islshpat  34304  lcvbr2  34309  lcvbr3  34310  lcvnbtwn2  34314  ellkr  34376  cvrval2  34561  cvrnbtwn2  34562  cvrnbtwn3  34563  cvrnbtwn4  34566  ishlat2  34640  lplnexatN  34849  islvol5  34865  dath  35022  pmapglb  35056  polval2N  35192  pclfinclN  35236  lhpexle3  35298  4atex2  35363  4atex2-0bOLDN  35365  isltrn2N  35406  cdleme0nex  35577  cdleme22b  35629  cdlemg17pq  35960  cdlemg19  35972  cdlemg21  35974  cdlemg33d  35997  dibopelvalN  36432  dibopelval2  36434  dib1dim  36454  dicelval2N  36471  diclspsn  36483  lcdlss  36908  mapd1o  36937  mzpcompact2lem  37314  fz1eqin  37332  rexrabdioph  37358  expdiophlem1  37588  dford4  37596  fnwe2lem2  37621  fgraphopab  37788  ifpidg  37836  rp-fakenanass  37860  rp-fakeinunass  37861  rp-isfinite6  37864  elinintrab  37883  elnonrel  37891  elmapintab  37902  dfrtrcl5  37936  imaiun1  37943  coiun1  37944  rfovcnvf1od  38298  andi3or  38320  uneqsn  38321  ntrneicls00  38387  2sbc5g  38617  pm14.12  38622  2sb5nd  38776  uun2221  39040  uun2221p1  39041  uun2221p2  39042  2sb5ndVD  39146  2sb5ndALT  39168  disjinfi  39380  climuz  39976  dfxlim2  40074  cncfshift  40087  dvnmul  40158  dvnprodlem2  40162  ismbl3  40203  ismbl4  40210  stoweidlem26  40243  stoweidlem35  40252  fourierdlem54  40377  fourierdlem83  40406  fourierdlem100  40423  fourierdlem104  40427  fourierdlem109  40432  fourierdlem112  40435  smfpimcc  41014  reuan  41180  2reu4a  41189  dfdfat2  41211  ffnaov  41279  iccpartiltu  41358  isrnghm  41892  2zrngmmgm  41946  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  opeliun2xp  42111  pgrpgt2nabl  42147  islindeps  42242  lindslinindsimp1  42246  lindslinindsimp2  42252  ldepslinc  42298  blen1b  42382  dffun3f  42429  setrec1lem3  42436  elpglem3  42456  elpg  42457