Theorem anbi1i 483

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 437	. 2 |- ((ph /\ ch) <-> (ch /\ ph))
2		bi.aa	. . 3 |- (ph <-> ps)
3	2	anbi2i 482	. 2 |- ((ch /\ ph) <-> (ch /\ ps))
4		ancom 437	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
5	1, 3, 4	3bitr 177	1 |- ((ph /\ ch) <-> (ps /\ ch))

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  anbi12i 484  pm5.53 485  an12 486  anandi 512  bibi2i 610  xor 673  prlem2 773  3ancoma 784  an6 904  19.28 1072  sb3an 1240  euan 1430  2eu6 1457  clabel 1585  r19.27av 1757  r19.29 1759  r19.41v 1766  rexcom 1778  gencbvex 1841  reu5 1932  rmo4 1936  ssrab 2128  inass 2226  dfun2 2246  symdif2 2269  inrab2 2275  reuun2 2281  undif4 2329  difin0ss 2336  iunid 2607  iunxsn 2617  iunxun 2619  zfrep4 2706  abssexg 2753  copsexg 2798  opeqsn 2808  opabid 2816  dfid3 2842  wefrc 2949  ordpwsuc 3072  dfom2 3139  opelxp 3220  xpundir 3232  brinxp2 3237  brres 3379  dmres 3386  resiexg 3402  iss 3403  imasng 3430  elimasn 3432  asymref 3445  asymref2 3446  elxp4 3459  elxp5 3460  dminss 3468  imainss 3469  ssrnres 3487  resco 3506  imaco 3507  coi1 3516  coass 3518  cnvpo 3528  dffun2 3532  fncnv 3567  funin 3572  imadif 3580  fcoi1 3651  fcoi2 3652  fcnvres 3654  f1o3 3700  f1ores 3709  ffoss 3717  f11o 3718  fv2 3726  tz6.12-1 3742  fvopabn 3792  fopabfv 3837  fsn 3840  fopabap 3847  imaiun 3870  abexssex 3878  f1ofv 3883  dfrdg2 3939  dfoprab2 3997  fnoprval 4023  foprval 4024  2ndconst 4103  elxp7 4109  dfopab2 4119  dfoprab3 4120  dfoprab5 4121  foprab2 4125  oarec 4202  dfec2 4270  snec 4302  oprec 4324  fvopabf4 4346  map0e 4348  domen 4385  mapsnen 4435  xpsnen 4441  xpcomen 4445  xpassen 4447  sbthlem9 4461  xpmapenlem5 4506  zfregs 4657  cp 4732  bnd2 4734  aceq5lem1 4745  aceq5lem2 4746  aceq5lem5 4749  kmlem3 4777  aceqkm 4791  zfcndrep 4978  ltexpi 5041  1pr 5129  distrlem5pr 5143  ltexprlem4 5157  reclem1pr 5168  reclem2pr 5169  addcnsr 5265  mulcnsr 5266  ltresr 5270  axrrecex 5296  lesub0 5624  divmul13t 5784  infm3 6056  infmsup 6070  elnnz 6147  elnn0z 6149  elioo3g 6381  rexuz2 6446  elfz2t 6473  elfzuzb 6477  fznn0t 6517  sqrval 6672  abslt 6875  absle 6876  cvgcmp3cetlem2 7189  isummulc1a 7214  infcvglem1 7221  geosum 7241  geoisum 7242  geoisum1 7244  cncfval 7264  efclt 7312  efcvgfsum 7315  erelem6 7324  efcj 7336  infpn2 7510  infxpidmlem7 7559  infxpidmlem9 7561  istps2 7608  istps3 7609  tgss3t 7637  ntrfval 7664  clsfval 7665  ntrval 7673  clsval 7674  neifval 7711  neif 7712  neival 7714  lpfval 7739  lpval 7740  cncnplem4 7774  dfms2 7796  blfval2 7833  blrn2 7839  blf 7841  cncfmet 7902  iscau 7933  bcthlem12 8007  sspval 8378  nmofval 8421  pilem1 8666  avril1 8779  h2hlm 8845  dfhnorm2 8983  hhsssh2 9135  ocvalt 9148  spanvalt 9294  hsupval2t 9295  sshjvalt 9315  sshjval3t 9321  hosmvalt 9506  hommvalt 9507  hodmvalt 9508  hfsmvalt 9509  hfmmvalt 9510  dmadjss 9814  nmcopexlem1 9946  nmcfnexlem1 9975  adjbdlnt 10011  cvnbtwn3t 10210  cvnbtwn4t 10211  irred 10316  sumdmdi 10337  symgoprab 10397  ntunte 10434  abfi 10443  hmeogrp 10524  blkssatm 10738

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 147  df-an 225

Copyright terms: Public domain