Theorem anbi2i 491

Description: Introduce a left conjunct to both sides of a logical equivalence.

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	. . . 4 |- (ph <-> ps)
2	1	biimpi 158	. . 3 |- (ph -> ps)
3	2	anim2i 342	. 2 |- ((ch /\ ph) -> (ch /\ ps))
4	1	biimpri 159	. . 3 |- (ps -> ph)
5	4	anim2i 342	. 2 |- ((ch /\ ps) -> (ch /\ ph))
6	3, 5	impbii 164	1 |- ((ch /\ ph) <-> (ch /\ ps))

Syntax hints:   <-> wb 153   /\ wa 230

This theorem is referenced by:  anbi1i 492  anbi12i 493  an23 496  an4 517  an42 518  anandir 522  3imtr3g 563  oranabs 593  bibi2i 619  xor2 684  rnlem 785  nic-justlem 968  19.27 1110  sb6 1309  3exdistr 1354  4exdistr 1355  eeeanv 1366  2sb5 1377  2sb5rf 1380  sbel2x 1387  eu2 1438  eu3 1439  mo4f 1444  eu5 1451  eu4 1452  euan 1470  2mos 1491  2eu4 1495  2eu6 1497  clelab 1628  r2ex 1738  reu2 1977  reu3 1978  reu4 1981  reu7 1982  sbc8g 2006  dfpss2 2184  dfpss3 2185  difdif 2217  inass 2274  dfss4 2293  dfin2 2295  difin 2296  indi 2302  difin0ss 2384  inssdif0 2385  eluniab 2567  unipr 2569  uniun 2573  uniin 2574  dfiun2g 2640  iunin2 2663  iundif2 2665  iindif2 2666  axrep1 2749  axrep4 2752  notzfaus 2796  eqvinop 2847  opeqsn 2858  opabid 2866  uniuni 2937  ordtri3or 3036  onzsl 3174  findsg 3214  tfindsg 3219  fconstopab 3267  xpundi 3282  elcnv2 3351  cnvuni 3358  dmuni 3376  opelres 3429  dfima3 3463  elima3 3467  imai 3474  asymref2 3497  intirr 3498  rnuni 3516  imainss 3520  ssrnres 3538  rninxp 3539  cores 3556  rnco 3559  coass 3569  dffun2 3583  dffun3 3584  dffun4 3585  dffun5 3586  dffunmof 3587  funeu2 3595  dffun6 3596  dffun8 3598  svrelfun 3617  fncnv 3618  funcnvuni 3621  imadif 3631  fcoi2 3703  fconst 3715  f11 3721  fores 3738  f1o4 3753  f1o5 3754  f1ocnv 3758  fvopab2 3848  eqfnfvf 3855  ffnfvf 3886  fsn2 3893  funiunfv 3923  f1fvf 3932  tfrlem2 3970  dfrdg2 3991  rdglem1 3995  tz7.49 4017  ffnoprval 4072  eqfnoprval 4074  fooprval 4095  2ndconst 4155  foprab2 4177  th3qlem1 4375  mapsnen 4490  xpassen 4504  pw2en 4509  xpmapenlem5 4565  abfii1 4621  abfii2 4622  inf2 4670  axinf 4685  trcl 4707  aceq1 4791  aceq3 4795  aceq4 4796  aceq5lem2 4798  aceq5lem3 4799  aceq5 4802  kmlem3 4829  kmlem4 4830  kmlem14 4840  kmlem15 4841  aceqkm 4843  zorn2lem7 4856  brdom7disj 4866  brdom6disj 4867  cf0 4975  zfcndrep 5031  zfcndinf 5035  distrlem1pr 5192  distrlem5pr 5196  opelreal 5314  elreal 5315  pre-axsup 5356  elnnz 6227  elznn0nn 6230  peano2uz2 6286  nnwof 6485  nnwos 6486  elfzuzb 6502  cau3iri 7005  cbvsumi 7076  clm1i 7167  climcmplem 7227  cvgcmp3cetlem1 7278  cvgcmp3cetlem2 7279  cvgratlem3 7342  elcncf1di 7360  infpn2 7601  infmap2lem1 7671  infmap2 7673  isbasis2g 7701  tgval2 7706  tgval3 7714  tgss3 7727  basgen 7729  subtop 7733  clsval2 7770  cncnp 7863  blfval2 7921  blf 7929  iscau2 8022  xpcn 8061  oprcn 8062  fsumcnlem 8074  bcthlem4 8087  bcthlem12 8095  bcthlem14 8097  bcthlem32 8115  sspval 8466  ubthlem1 8613  spwval2 8737  spwmo 8740  pilem1 8754  axgroth4 8863  grothprim 8866  hlimcauii 9189  ocsh 9239  pjtheui 9318  shscli 9364  h1deoi 9555  h1dei 9556  hommval 9595  hfmmval 9598  nmcopexlem1 10034  nmcopexlem2 10035  nmcfnexlem1 10063  nmcfnexlem2 10064  pjhmopidm 10193  cvbr2 10294  cvnbtwn2 10298  cvnbtwn4 10300  mdsl2i 10333  cvmdi 10335  mdsymlem6 10419  cdj3lem3b 10451  ahypfmbi 10513  eeeeanv 10522  ishgrag 10853

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

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain