Theorem anbi1i 481

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 435	. 2 |- ((ph /\ ch) <-> (ch /\ ph))
2		bi.aa	. . 3 |- (ph <-> ps)
3	2	anbi2i 480	. 2 |- ((ch /\ ph) <-> (ch /\ ps))
4		ancom 435	. 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 482  pm5.53 483  an12 484  anandi 510  bibi2i 607  xor 670  prlem2 770  3ancoma 781  an6 900  19.28 1068  sb3an 1236  euan 1426  2eu6 1452  clabel 1579  r19.27av 1751  r19.29 1753  r19.41v 1760  rexcom 1772  gencbvex 1834  reu5 1925  rmo4 1929  ssrab 2121  inass 2219  dfun2 2239  symdif2 2262  inrab2 2268  reuun2 2274  undif4 2321  difin0ss 2328  iunid 2598  iunxsn 2607  iunxun 2609  zfrep4 2696  abssexg 2742  copsexg 2787  opeqsn 2797  opabid 2805  dfid3 2831  wefrc 2938  ordpwsuc 3061  dfom2 3128  opelxp 3209  xpundir 3221  brinxp2 3226  brres 3365  dmres 3372  resiexg 3388  iss 3389  imasng 3416  elimasn 3418  asymref 3431  asymref2 3432  elxp4 3445  elxp5 3446  dminss 3454  imainss 3455  ssrnres 3473  resco 3492  imaco 3493  coi1 3502  coass 3504  cnvpo 3514  dffun2 3518  fncnv 3553  funin 3558  imadif 3566  fcoi1 3636  fcoi2 3637  fcnvres 3639  f1o3 3685  f1ores 3694  ffoss 3702  f11o 3703  fv2 3711  tz6.12-1 3727  fvopabn 3777  fopabfv 3822  fsn 3825  fopabap 3832  imaiun 3855  abexssex 3863  f1ofv 3868  dfrdg2 3924  dfoprab2 3982  fnoprval 4008  foprval 4009  2ndconst 4087  elxp7 4093  dfopab2 4103  dfoprab3 4104  dfoprab5 4105  foprab2 4109  oarec 4186  dfec2 4254  snec 4286  oprec 4308  fvopabf4 4330  map0e 4332  domen 4367  mapsnen 4416  xpsnen 4421  xpcomen 4425  xpassen 4427  sbthlem9 4441  xpmapenlem5 4486  abfii2 4542  zfregs 4627  cp 4702  bnd2 4704  aceq5lem1 4715  aceq5lem2 4716  aceq5lem5 4719  kmlem3 4747  aceqkm 4761  zfcndrep 4946  ltexpi 5009  1pr 5097  distrlem5pr 5111  ltexprlem4 5125  reclem1pr 5136  reclem2pr 5137  addcnsr 5233  mulcnsr 5234  ltresr 5238  axrrecex 5264  lesub0 5594  divmul13t 5746  infm3 6009  infmsup 6023  elnnz 6100  elnn0z 6102  elioo3g 6325  rexuz2 6385  elfz2t 6412  elfzuzb 6416  fznn0t 6456  sqrval 6609  abslt 6818  absle 6819  cvgcmp3cetlem2 7133  isummulc1a 7157  infcvglem1 7164  geosum 7184  geoisum 7185  geoisum1 7187  cncfval 7207  efclt 7262  efcvgfsum 7265  erelem6 7274  efcj 7286  infpn2 7460  infxpidmlem7 7509  infxpidmlem9 7511  istps2 7557  istps3 7558  istps5 7560  tgss3t 7588  ntrfval 7617  clsfval 7618  ntrval 7626  clsval 7627  neifval 7664  neif 7665  neival 7667  lpfval 7692  lpval 7693  cncnplem4 7727  dfms2 7749  blfval2 7788  blrn2 7794  blf 7796  cncfmet 7857  iscau 7888  bcthlem12 7960  sspval 8329  nmofval 8370  pilem1 8609  avril1 8723  h2hlm 8789  dfhnorm2 8927  hhsssh2 9079  ocvalt 9092  spanvalt 9237  hsupval2t 9238  sshjvalt 9258  sshjval3t 9264  hosmvalt 9451  hommvalt 9452  hodmvalt 9453  hfsmvalt 9454  hfmmvalt 9455  dmadjss 9759  nmcopexlem1 9889  nmcfnexlem1 9918  adjbdlnt 9954  cvnbtwn3t 10153  cvnbtwn4t 10154  irred 10258  sumdmdi 10278  symgoprab 10336  ntunte 10376  abfi 10385  hmeogrp 10461  blkssatm 10639

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