Theorem anbi2i 538

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 168	. . 3 |- (ph -> ps)
3	2	anim2i 362	. 2 |- ((ch /\ ph) -> (ch /\ ps))
4	1	biimpri 169	. . 3 |- (ps -> ph)
5	4	anim2i 362	. 2 |- ((ch /\ ps) -> (ch /\ ph))
6	3, 5	impbii 174	1 |- ((ch /\ ph) <-> (ch /\ ps))

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  anbi1i 539  anbi12i 540  an23 543  an4 564  an42 565  anandir 569  3imtr3g 611  oranabs 642  bibi2iOLD 670  xor2 736  rnlemOLD 854  nic-justlem 1231  nic-mpALT 1238  nic-axALT 1240  19.27 1419  sb6 1644  3exdistr 1693  3exdistrOLD 1694  4exdistr 1695  eeeanvOLD 1709  2sb5 1725  2sb5rf 1728  sbel2x 1736  eu2 1791  eu3 1792  mo4f 1798  eu5 1805  eu4 1806  euan 1827  euanOLD 1828  2mos 1852  2eu4 1856  2eu6 1858  clelab 2013  nonconne 2023  r2ex 2152  ceqsex3v 2330  ceqsex4v 2331  ceqsex8v 2333  reu2 2442  reu6 2443  reu4 2446  reu7 2447  sbc8gOLD 2478  dfpss2 2694  dfpss3OLD 2696  difdif 2734  inass 2804  dfss4 2827  dfss4OLD 2828  dfin2 2830  difinOLD 2832  indi 2838  indiOLD 2839  difin0ss 2939  inssdif0 2940  inssdif0OLD 2941  eluniab 3189  unipr 3191  uniun 3196  uniin 3197  uniinOLD 3198  dfiun2gOLD 3284  iunin2 3320  iundif2 3322  iindif2 3324  axrep1 3429  axrep4 3432  notzfaus 3478  eqvinop 3536  opcom 3547  opeqsn 3549  opabidOLD 3558  ordtri3or 3691  ordtri3orOLD 3692  trsuc2 3754  uniuni 3806  eufromeq2 3829  eufromeq6 3833  onzslOLD 3929  tfindsg 3944  findsg 3980  fconstopab 4031  xpundi 4050  elvvv 4054  elcnv2 4138  cnvuni 4147  dmuni 4166  opelres 4222  dfima3OLD 4268  elima3 4272  imai 4280  asymref 4308  asymref2OLD 4311  intirrOLD 4313  rnuni 4327  imainss 4331  ssrnres 4354  rninxpOLD 4356  coundir 4398  coundirOLD 4399  coresOLD 4401  rnco 4404  coass 4415  relrelss 4417  dffun2 4431  dffun3 4432  dffun4 4433  dffun5 4434  dffun6f 4435  funeu2 4446  dffun7 4447  dffun8 4448  dffun9 4450  svrelfun 4478  fncnv 4479  funcnvuni 4482  imadif 4493  iunfopab 4542  fcoi2OLD 4587  fint 4591  fin 4593  fconstOLD 4603  dff12 4609  fores 4627  dff1o4 4644  dff1o4OLD 4645  dff1o5OLD 4647  f1ocnvOLD 4652  fvopab2 4754  eqfnfv3 4769  ffnfvf 4802  fsn2 4809  funiunfv 4842  dff13f 4851  ffnoprv 4943  eqfnoprv 4945  fooprv 4967  foprab2 5061  tfrlem2 5120  dfrdg2 5141  rdglem1 5145  tz7.49 5168  th3qlem1 5373  mapsnen 5488  xpassen 5500  pw2en 5505  xpmapenlem5 5594  abfii1 5651  abfii2 5652  ordtypelem4 5687  dford2 5711  inf2 5714  zfinf 5729  trcl 5752  aceq1 5891  aceq3 5895  aceq4 5896  aceq5lem2 5898  aceq5lem3 5899  aceq5 5902  kmlem3 5929  kmlem4 5930  kmlem14 5940  kmlem15 5941  aceqkm 5943  zorn2lem7 5956  brdom7disj 5966  brdom6disj 5967  cf0 6058  zfcndrep 6118  zfcndinf 6122  distrlem1pr 6279  distrlem5pr 6283  opelreal 6401  elreal 6402  pre-axsup 6444  elnnz 7354  elznn0nn 7357  peano2uz2 7413  nnwof 7628  nnwos 7629  elfzuzb 7646  fzsuc 7678  cau3iri 8167  cbvsumi 8246  clm1i 8337  climcmplem 8397  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  cvgratlem3 8514  elcncf1di 8532  infpn2 8778  infmap2lem1 8848  infmap2 8850  istop2g 8866  istps4 8878  isbasis2g 8881  tgval2 8887  tgval3 8895  tgss3 8908  basgen 8910  subtop 8916  fctop2 8921  clsval2 8961  cncnp 9055  blfval2 9113  blf 9121  iscau2 9215  xpcn 9254  oprcn 9255  fsumcnlem 9267  bcthlem4 9280  bcthlem12 9288  bcthlem14 9290  bcthlem32 9308  gapmlem 9461  gapm 9462  sspval 9721  ubthlem1 9872  spwval2 9996  spwmo 9999  pilem1 10020  axgroth4 10139  grothprim 10141  oprab2co 10160  isfbas2 10263  elfg 10284  hausfillim 10303  hlimcauii 10739  ocsh 10789  pjtheui 10868  shscli 10914  h1deoi 11105  h1dei 11106  hommval 11145  hfmmval 11148  nmcopexlem1 11588  nmcopexlem2 11589  nmcfnexlem1 11617  nmcfnexlem2 11618  pjhmopidm 11754  cvbr2 11855  cvnbtwn2 11859  cvnbtwn4 11861  mdsl2i 11894  cvmdi 11896  mdsymlem6 11980  cdj3lem3b 12012  bnj173OLD 12041  bnj174OLD 12043  bnj184OLD 12055  bnj251 12090  bnj252 12091  bnj257 12096  bnj279OLD 12119  bnj290 12130  bnj301OLD 12142  bnj411OLD 12259  bnj422OLD 12271  bnj445OLD 12295  bnj456OLD 12307  bnj467OLD 12319  bnj490OLD 12343  bnj500OLD 12355  bnj11OLD 12377  bnj26 12389  bnj29 12394  bnj30 12395  bnj30OLD 12396  bnj54 12428  bnj112 12457  bnj142 12474  bnj158 12483  bnj512 12519  bnj869 12797  bnj888 12811  bnj962 12856  bnj1061 12898  bnj1166 12958  bnj1183 12965  bnj1192 12969  bnj1215 12991  bnj1222 12995  bnj153 13247  bnj543 13269  bnj545 13271  bnj571 13289  bnj582 13295  bnj607 13304  bnj882 13320  bnj987 13361  bnj1033 13384  bnj1067 13399  bnj1253 13470  bnj1462 13546  bnj1463 13550  divalglem10 13705  ndvdssub 13710  algcvgblem 13745  isprm2 13775  axinfprim 13790  axacprim 13791  trsuc2OLD 13793  indifdi 13823  dford3 13848  dfon2lem5 13853  dfon2 13858  wfi 13915  frind 13939  soxp 13950  frxp 13951  tfrALTlem 13976  frr3g 13980  axfelem9 14039  axfelem14 14044  brtxp 14067  elfix 14077  df3nandALT1 14146  andnand1 14148  nandsym1 14246  and4com 14267  eeeeanv 14272  tostos 14637  dfdir2 14639  cbvprodi 14662  vecval1b 14794  trhom 14983  altretoplem2 14996  altretop 14997  issubcat 15193  settrcon 15247  tarval2 15249  cnvresima 15359  trer 15361  ordtypelem4OLD 15378  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  is1stc3 15469  isfne2 15481  isfne3 15482  fneerdm 15498  locfincomp 15514  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem4 15522  neifg 15559  ufinffr 15578  fmfnfm 15598  fcluscf 15612  flimfnfcls 15615  inpreima 15682  unpreima 15683  opabex3 15701  opropabco 15712  f1opr 15714  eqfnfv3OLD 15721  cbvixp 15723  fimax 15746  fzsplit 15792  fzm1 15796  sdc 15811  txcnoprab 15911  heiborlem1 15955  phtpycom 16050  pcorevlem 16086  isdivrng1 16109  keridl 16180  ispridlc 16218  an43OLD 16236  prtlem70 16238  prtlem100 16244  prtlem5 16245  prtlem15 16281  prter3 16286  ishgrag 16291  strdif 16719  isposNEW 16773  isopos 16909  cvrval2 16991  cvrnbtwn2 16992  cvrnbtwn3 16993  cvrnbtwn4 16996  isgrpNEW 17104  grpclNEW 17106  isringNEW 17142  ringclNEW 17144  islvec 17188  pmapglb 17252  polval2 17319

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 164  df-an 242

Copyright terms: Public domain