Theorem anbi2i 483

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 149	. . 3 |- (ph -> ps)
3	2	anim2i 333	. 2 |- ((ch /\ ph) -> (ch /\ ps))
4	1	biimpri 150	. . 3 |- (ps -> ph)
5	4	anim2i 333	. 2 |- ((ch /\ ps) -> (ch /\ ph))
6	3, 5	impbii 155	1 |- ((ch /\ ph) <-> (ch /\ ps))

Syntax hints:   <-> wb 144   /\ wa 221

This theorem is referenced by:  anbi1i 484  anbi12i 485  an23 488  an4 509  an42 510  anandir 514  3imtr3g 555  oranabs 585  bibi2i 611  xor2 676  rnlem 778  nic-justlem 961  nic-mpALT 968  nic-axALT 970  19.27 1105  sb6 1305  3exdistr 1350  4exdistr 1351  eeeanv 1362  2sb5 1374  2sb5rf 1377  sbel2x 1384  eu2 1435  eu3 1436  mo4f 1441  eu5 1448  eu4 1449  euan 1467  2mos 1488  2eu4 1492  2eu6 1494  clelab 1624  r2ex 1737  reu2 1976  reu3 1977  reu4 1980  reu7 1981  sbc8g 2004  dfpss2 2185  dfpss3 2186  difdif 2218  inass 2275  dfss4 2294  dfin2 2296  difin 2297  indi 2303  difin0ss 2385  inssdif0 2386  eluniab 2579  unipr 2581  uniun 2586  uniin 2587  dfiun2g 2654  iunin2 2677  iundif2 2679  iindif2 2681  axrep1 2768  axrep4 2771  notzfaus 2815  eqvinop 2867  opcom 2877  opeqsn 2879  opabid 2887  ordtri3or 3007  uniuni 3104  onzsl 3200  tfindsg 3213  findsg 3245  fconstopab 3293  xpundi 3310  elvvv 3314  elcnv2 3385  cnvuni 3392  dmuni 3410  opelres 3459  dfima3 3498  elima3 3502  imai 3509  asymref2 3532  intirr 3533  rnuni 3544  imainss 3548  ssrnres 3566  rninxp 3567  coundir 3601  cores 3602  rnco 3605  coass 3616  relrelss 3618  dffun2 3631  dffun3 3632  dffun4 3633  dffun5 3634  dffun6f 3635  funeu2 3643  dffun7 3644  dffun9 3646  svrelfun 3665  fncnv 3666  funcnvuni 3669  imadif 3679  fcoi2 3753  fconst 3765  dff12 3771  fores 3789  dff1o4 3804  dff1o5 3805  f1ocnv 3809  fvopab2 3902  ffnfvf 3943  fsn2 3950  funiunfv 3980  dff13f 3989  ffnoprv 4074  eqfnoprv 4076  fooprv 4098  foprab2 4181  tfrlem2 4213  dfrdg2 4234  rdglem1 4238  tz7.49 4260  th3qlem1 4455  mapsnen 4570  xpassen 4582  pw2en 4587  xpmapenlem5 4647  abfii1 4704  abfii2 4705  inf2 4753  zfinf 4768  trcl 4791  aceq1 4875  aceq3 4879  aceq4 4880  aceq5lem2 4882  aceq5lem3 4883  aceq5 4886  kmlem3 4913  kmlem4 4914  kmlem14 4924  kmlem15 4925  aceqkm 4927  zorn2lem7 4940  brdom7disj 4950  brdom6disj 4951  cf0 5060  zfcndrep 5120  zfcndinf 5124  distrlem1pr 5281  distrlem5pr 5285  opelreal 5403  elreal 5404  pre-axsup 5445  elnnz 6313  elznn0nn 6316  peano2uz2 6372  nnwof 6586  nnwos 6587  elfzuzb 6604  fzsuc 6636  cau3iri 7118  cbvsumi 7189  clm1i 7280  climcmplem 7340  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  cvgratlem3 7457  elcncf1di 7475  infpn2 7721  infmap2lem1 7791  infmap2 7793  istop2g 7809  istps4 7821  isbasis2g 7824  tgval2 7829  tgval3 7837  tgss3 7850  basgen 7852  subtop 7858  clsval2 7895  cncnp 7988  blfval2 8046  blf 8054  iscau2 8148  xpcn 8187  oprcn 8188  fsumcnlem 8200  bcthlem4 8213  bcthlem12 8221  bcthlem14 8223  bcthlem32 8241  sspval 8636  ubthlem1 8787  spwval2 8915  spwmo 8918  pilem1 8938  axgroth4 9052  grothprim 9057  hlimcauii 9382  ocsh 9432  pjtheui 9511  shscli 9557  h1deoi 9748  h1dei 9749  hommval 9788  hfmmval 9791  nmcopexlem1 10230  nmcopexlem2 10231  nmcfnexlem1 10259  nmcfnexlem2 10260  pjhmopidm 10390  cvbr2 10491  cvnbtwn2 10495  cvnbtwn4 10497  mdsl2i 10530  cvmdi 10532  mdsymlem6 10617  cdj3lem3b 10649  ahypfmbi 10711  eeeeanv 10720  tostos 10883  altretoplem2 11143  altretop 11144  issubcat 11299  cnvresima 11407  trer 11409  ordtypelem4 11430  compfipin0 11493  alexsublem2 11497  alexsublem3 11498  is1stc3 11530  isfne2 11542  isfne3 11543  fneerdm 11559  locfincomp 11575  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem4 11583  isfbas2 11622  elfg 11633  neifg 11644  ufinffr 11663  hausfillim 11685  fmfnfm 11704  fcluscf 11724  flimfnfcls 11727  gapmlem 11783  gapm 11784  inpreima 11793  unpreima 11794  opabex3 11806  oprab2co 11812  eqfnfv3 11819  cbvixpv 11821  fimax 11837  fzm1 11867  sdc 11877  txcnoprab 11981  heiborlem1 12011  phtpycom 12092  ishgrag 12195

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 145  df-an 223

Copyright terms: Public domain