Theorem anbi1i 492

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

Hypothesis

Ref	Expression
bi.aa	|- (ph <-> ps)

Assertion

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

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		ancom 446	. 2 |- ((ph /\ ch) <-> (ch /\ ph))
2		bi.aa	. . 3 |- (ph <-> ps)
3	2	anbi2i 491	. 2 |- ((ch /\ ph) <-> (ch /\ ps))
4		ancom 446	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
5	1, 3, 4	3bitri 184	1 |- ((ph /\ ch) <-> (ps /\ ch))

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

This theorem is referenced by:  anbi12i 493  pm5.53 494  an12 495  anandi 521  bibi2i 619  xor 682  prlem2 783  3ancoma 794  an6 914  19.28 1111  sb3an 1280  euan 1470  2eu6 1497  clabel 1629  r19.27av 1801  r19.29 1803  r19.41v 1810  rexcom 1822  gencbvex 1885  reu5 1976  rmo4 1980  ssrab 2176  inass 2274  dfun2 2294  symdif2 2317  inrab2 2323  reuun2 2329  undif4 2377  difin0ss 2384  iunid 2657  iunxsn 2667  iunxun 2669  zfrep4 2756  abssexg 2803  copsexg 2848  opeqsn 2858  opabid 2866  dfid3 2892  wefrc 3000  ordpwsuc 3123  dfom2 3190  opelxp 3271  xpundir 3283  brinxp2 3288  brres 3430  dmres 3437  resiexg 3453  iss 3454  imasng 3481  elimasn 3483  asymref 3496  asymref2 3497  elxp4 3510  elxp5 3511  dminss 3519  imainss 3520  ssrnres 3538  resco 3557  imaco 3558  coi1 3567  coass 3569  cnvpo 3579  dffun2 3583  fncnv 3618  funin 3623  imadif 3631  fcoi1 3702  fcoi2 3703  fcnvres 3705  f1o3 3751  f1ores 3760  ffoss 3768  f11o 3769  fv2 3777  tz6.12-1 3793  fvopabn 3843  fopabfv 3888  fsn 3891  fopabap 3898  imaiun 3921  abexssex 3929  f1ofv 3935  dfrdg2 3991  dfoprab2 4049  fnoprval 4075  foprval 4076  2ndconst 4155  elxp7 4161  dfopab2 4171  dfoprab3 4172  dfoprab5 4173  foprab2 4177  oarec 4254  dfec2 4322  uniqs 4356  snec 4357  oprec 4379  fvopabf4 4401  map0e 4403  domen 4440  mapsnen 4490  xpsnen 4498  xpcomen 4502  xpassen 4504  sbthlem9 4518  xpmapenlem5 4565  abfii2 4622  zfregs 4709  cp 4784  bnd2 4786  aceq5lem1 4797  aceq5lem2 4798  aceq5lem5 4801  kmlem3 4829  aceqkm 4843  zfcndrep 5031  ltexpi 5094  1pr 5182  distrlem5pr 5196  ltexprlem4 5210  reclem1pr 5221  reclem2pr 5222  addcnsr 5318  mulcnsr 5319  ltresr 5323  axrrecex 5349  lesub0i 5677  divmul13 5840  infm3 6136  infmsup 6150  elnnz 6227  elnn0z 6229  irradd 6329  elioo3g 6405  rexuz2 6471  elfz2 6498  elfzuzb 6502  fznn0 6542  sqrval 6761  abslti 6965  abslei 6966  cvgcmp3cetlem2 7279  isummulc1ai 7304  infcvglem1 7311  geosumi 7331  geoisum 7332  geoisum1 7334  cncfval 7354  efcl 7402  efcvgfsum 7405  erelem6 7414  efcji 7426  infpn2 7601  infxpidmlem7 7650  infxpidmlem9 7652  istps2 7698  istps3 7699  tgss3 7727  ntrfval 7752  clsfval 7753  ntrval 7761  clsval 7762  neifval 7799  neif 7800  neival 7802  lpfval 7827  lpval 7828  cncnplem4 7862  dfms2 7884  blfval2 7921  blrn2 7927  blf 7929  cncfmet 7990  iscau 8021  bcthlem12 8095  sspval 8466  nmofval 8509  pilem1 8754  avril1 8867  h2hlm 8933  dfhnorm2 9071  hhsssh2 9223  ocval 9236  spanval 9382  hsupval2 9383  sshjval 9403  sshjval3 9409  hosmval 9594  hommval 9595  hodmval 9596  hfsmval 9597  hfmmval 9598  dmadjss 9902  nmcopexlem1 10034  nmcfnexlem1 10063  adjbdln 10099  cvnbtwn3 10299  cvnbtwn4 10300  irredi 10405  sumdmdii 10426  symgoprab 10487  ntunte 10525  abfi 10534  hmeogrp 10632  blkssatm 10851

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