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 608  xor 671  prlem2 771  3ancoma 782  an6 902  19.28 1070  sb3an 1238  euan 1428  2eu6 1454  clabel 1581  r19.27av 1753  r19.29 1755  r19.41v 1762  rexcom 1774  gencbvex 1836  reu5 1927  rmo4 1931  ssrab 2123  inass 2221  dfun2 2241  symdif2 2264  inrab2 2270  reuun2 2276  undif4 2323  difin0ss 2330  iunid 2601  iunxsn 2610  iunxun 2612  zfrep4 2699  abssexg 2745  copsexg 2790  opeqsn 2800  opabid 2808  dfid3 2834  wefrc 2941  ordpwsuc 3064  dfom2 3131  opelxp 3212  xpundir 3224  brinxp2 3229  brres 3371  dmres 3378  resiexg 3394  iss 3395  imasng 3422  elimasn 3424  asymref 3437  asymref2 3438  elxp4 3451  elxp5 3452  dminss 3460  imainss 3461  ssrnres 3479  resco 3498  imaco 3499  coi1 3508  coass 3510  cnvpo 3520  dffun2 3524  fncnv 3559  funin 3564  imadif 3572  fcoi1 3643  fcoi2 3644  fcnvres 3646  f1o3 3692  f1ores 3701  ffoss 3709  f11o 3710  fv2 3718  tz6.12-1 3734  fvopabn 3784  fopabfv 3829  fsn 3832  fopabap 3839  imaiun 3862  abexssex 3870  f1ofv 3875  dfrdg2 3931  dfoprab2 3989  fnoprval 4015  foprval 4016  2ndconst 4095  elxp7 4101  dfopab2 4111  dfoprab3 4112  dfoprab5 4113  foprab2 4117  oarec 4194  dfec2 4262  snec 4294  oprec 4316  fvopabf4 4338  map0e 4340  domen 4375  mapsnen 4424  xpsnen 4429  xpcomen 4433  xpassen 4435  sbthlem9 4449  xpmapenlem5 4494  abfii2 4550  zfregs 4635  cp 4710  bnd2 4712  aceq5lem1 4723  aceq5lem2 4724  aceq5lem5 4727  kmlem3 4755  aceqkm 4769  zfcndrep 4954  ltexpi 5017  1pr 5105  distrlem5pr 5119  ltexprlem4 5133  reclem1pr 5144  reclem2pr 5145  addcnsr 5241  mulcnsr 5242  ltresr 5246  axrrecex 5272  lesub0 5600  divmul13t 5753  infm3 6022  infmsup 6036  elnnz 6113  elnn0z 6115  elioo3g 6344  rexuz2 6405  elfz2t 6432  elfzuzb 6436  fznn0t 6476  sqrval 6631  abslt 6833  absle 6834  cvgcmp3cetlem2 7147  isummulc1a 7172  infcvglem1 7179  geosum 7199  geoisum 7200  geoisum1 7202  cncfval 7222  efclt 7270  efcvgfsum 7273  erelem6 7282  efcj 7294  infpn2 7466  infxpidmlem7 7515  infxpidmlem9 7517  istps2 7564  istps3 7565  istps5 7567  tgss3t 7595  ntrfval 7624  clsfval 7625  ntrval 7633  clsval 7634  neifval 7671  neif 7672  neival 7674  lpfval 7699  lpval 7700  cncnplem4 7734  dfms2 7756  blfval2 7793  blrn2 7799  blf 7801  cncfmet 7862  iscau 7893  bcthlem12 7967  sspval 8339  nmofval 8382  pilem1 8628  avril1 8739  h2hlm 8805  dfhnorm2 8943  hhsssh2 9095  ocvalt 9108  spanvalt 9254  hsupval2t 9255  sshjvalt 9275  sshjval3t 9281  hosmvalt 9466  hommvalt 9467  hodmvalt 9468  hfsmvalt 9469  hfmmvalt 9470  dmadjss 9774  nmcopexlem1 9906  nmcfnexlem1 9935  adjbdlnt 9971  cvnbtwn3t 10170  cvnbtwn4t 10171  irred 10276  sumdmdi 10297  symgoprab 10357  ntunte 10394  abfi 10403  hmeogrp 10480  blkssatm 10672

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