Theorem anbi1i 484

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

Hypothesis

Ref	Expression
bi.aa	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
anbi1i	⊢ ((φ ⋀ χ) ↔ (ψ ⋀ χ))

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		ancom 438	. 2 ⊢ ((φ ⋀ χ) ↔ (χ ⋀ φ))
2		bi.aa	. . 3 ⊢ (φ ↔ ψ)
3	2	anbi2i 483	. 2 ⊢ ((χ ⋀ φ) ↔ (χ ⋀ ψ))
4		ancom 438	. 2 ⊢ ((χ ⋀ ψ) ↔ (ψ ⋀ χ))
5	1, 3, 4	3bitri 177	1 ⊢ ((φ ⋀ χ) ↔ (ψ ⋀ χ))

Syntax hints:   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  anbi12i 485  pm5.53 486  an12 487  anandi 513  bibi2i 611  xor 674  prlem2 775  3ancoma 786  an6 906  19.28 1074  sb3an 1242  euan 1432  2eu6 1459  clabel 1589  r19.27av 1761  r19.29 1763  r19.41v 1770  rexcom 1782  gencbvex 1845  reu5 1936  rmo4 1940  ssrab 2136  inass 2234  dfun2 2254  symdif2 2277  inrab2 2283  reuun2 2289  undif4 2337  difin0ss 2344  iunid 2617  iunxsn 2627  iunxun 2629  zfrep4 2716  abssexg 2763  copsexg 2808  opeqsn 2818  opabid 2826  dfid3 2852  wefrc 2959  ordpwsuc 3082  dfom2 3149  opelxp 3230  xpundir 3242  brinxp2 3247  brres 3389  dmres 3396  resiexg 3412  iss 3413  imasng 3440  elimasn 3442  asymref 3455  asymref2 3456  elxp4 3469  elxp5 3470  dminss 3478  imainss 3479  ssrnres 3497  resco 3516  imaco 3517  coi1 3526  coass 3528  cnvpo 3538  dffun2 3542  fncnv 3577  funin 3582  imadif 3590  fcoi1 3661  fcoi2 3662  fcnvres 3664  f1o3 3710  f1ores 3719  ffoss 3727  f11o 3728  fv2 3736  tz6.12-1 3752  fvopabn 3802  fopabfv 3847  fsn 3850  fopabap 3857  imaiun 3880  abexssex 3888  f1ofv 3893  dfrdg2 3949  dfoprab2 4007  fnoprval 4033  foprval 4034  2ndconst 4113  elxp7 4119  dfopab2 4129  dfoprab3 4130  dfoprab5 4131  foprab2 4135  oarec 4212  dfec2 4280  snec 4314  oprec 4336  fvopabf4 4358  map0e 4360  domen 4397  mapsnen 4447  xpsnen 4454  xpcomen 4458  xpassen 4460  sbthlem9 4474  xpmapenlem5 4520  abfii2 4577  zfregs 4664  cp 4739  bnd2 4741  aceq5lem1 4752  aceq5lem2 4753  aceq5lem5 4756  kmlem3 4784  aceqkm 4798  zfcndrep 4986  ltexpi 5049  1pr 5137  distrlem5pr 5151  ltexprlem4 5165  reclem1pr 5176  reclem2pr 5177  addcnsr 5273  mulcnsr 5274  ltresr 5278  axrrecex 5304  lesub0i 5632  divmul13 5794  infm3 6086  infmsup 6100  elnnz 6177  elnn0z 6179  elioo3g 6347  rexuz2 6413  elfz2 6440  elfzuzb 6444  fznn0 6484  sqrval 6703  abslti 6907  abslei 6908  cvgcmp3cetlem2 7221  isummulc1ai 7246  infcvglem1 7253  geosumi 7273  geoisum 7274  geoisum1 7276  cncfval 7296  efcl 7344  efcvgfsum 7347  erelem6 7356  efcji 7368  infpn2 7542  infxpidmlem7 7591  infxpidmlem9 7593  istps2 7639  istps3 7640  tgss3 7668  ntrfval 7693  clsfval 7694  ntrval 7702  clsval 7703  neifval 7740  neif 7741  neival 7743  lpfval 7768  lpval 7769  cncnplem4 7803  dfms2 7825  blfval2 7862  blrn2 7868  blf 7870  cncfmet 7931  iscau 7962  bcthlem12 8036  sspval 8407  nmofval 8450  pilem1 8695  avril1 8808  h2hlm 8874  dfhnorm2 9012  hhsssh2 9164  ocval 9177  spanval 9323  hsupval2 9324  sshjval 9344  sshjval3 9350  hosmval 9535  hommval 9536  hodmval 9537  hfsmval 9538  hfmmval 9539  dmadjss 9843  nmcopexlem1 9975  nmcfnexlem1 10004  adjbdln 10040  cvnbtwn3 10240  cvnbtwn4 10241  irredi 10346  sumdmdii 10367  symgoprab 10427  ntunte 10464  abfi 10473  hmeogrp 10571  blkssatm 10790

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