Theorem ancom 435

Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118.

Assertion

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

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		pm3.27 323	. . 3 |- ((ph /\ ps) -> ps)
2		pm3.26 319	. . 3 |- ((ph /\ ps) -> ph)
3	1, 2	jca 288	. 2 |- ((ph /\ ps) -> (ps /\ ph))
4		pm3.27 323	. . 3 |- ((ps /\ ph) -> ph)
5		pm3.26 319	. . 3 |- ((ps /\ ph) -> ps)
6	4, 5	jca 288	. 2 |- ((ps /\ ph) -> (ph /\ ps))
7	3, 6	impbi 157	1 |- ((ph /\ ps) <-> (ps /\ ph))

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

This theorem is referenced by:  ancoms 436  ancomsd 437  pm3.22 438  anbi1i 481  an12 484  an23 485  anabs5 493  an42 507  bicom 519  andir 604  anbi1d 616  pm4.71r 635  pm5.32ri 645  pm5.32rd 647  xor 670  xor2 672  biantrurd 726  consensus 766  rnlem 772  3anrot 779  3ancoma 781  exancom 1052  19.29r 1070  19.42 1094  exan 1104  eu1 1390  mooran1 1423  moaneu 1428  moanmo 1429  2eu3 1449  2eu6 1452  2eu7 1453  2eu8 1454  eq2tr 1530  clabel 1579  r19.28av 1752  r19.29r 1754  r19.42v 1761  rabswap 1768  ralcom 1771  rexcom 1772  gencbvex 1834  euxfr2 1922  rmo4 1929  reu8 1932  incom 2204  symdif2 2262  difin0ss 2328  iunid 2598  moabex 2761  eqvinop 2786  dfid3 2831  uniuni 2875  reuxfr2 2898  ordtri4 2979  ordpwsuc 3061  elxp2 3198  cnvco 3295  dmuni 3314  dfima2 3397  imadmrn 3406  imai 3409  asymref 3431  intirr 3433  cnvsn 3441  rnuni 3451  cnvxp 3456  rninxp 3474  cores 3491  rnco 3494  cnvpo 3514  fncnv 3553  fununi 3555  funin 3558  f1cnv 3657  tz6.12-1 3727  fsn 3825  isoini 3891  tfrlem7 3908  ndmoprcom 4039  2ndconst 4087  oaord 4171  pmex 4317  mapval2 4325  mapsnen 4416  map1 4417  xpsnen 4421  xpcomen 4425  pw2en 4432  mapxpen 4481  cp 4702  aceq5lem1 4715  aceq5lem2 4716  aceq5lem3 4717  aceq6b 4722  kmlem3 4747  brdom7disj 4784  brdom6disj 4785  cf0 4890  genpass 5092  1pr 5097  addcompr 5103  mulcompr 5105  reclem2pr 5137  elreal 5230  ltxrt 5475  letri3t 5498  lesub0 5594  addgtge0t 5630  divmul13t 5746  divmul24t 5747  divdivdivt 5749  ioonegt 6347  iccnegt 6348  icounlem 6353  indstr 6401  elfzuzb 6416  elfzuz2t 6426  fzrevt 6451  lenegsqt 6831  cau5 6864  sumex 6927  clm4 7026  sinbndt 7415  cosbndt 7416  znnen 7453  infpn2 7460  infxpidmlem9 7511  istps3 7558  tgval3t 7575  tgss3t 7588  clsval2 7635  metxp 7786  issubg 8068  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  h2hcau 8788  shorth 9107  5oalem2 9540  3oalem2 9548  mdsldmd1 10195  chrelat 10228  cvexchlem 10232  mdsymlem8 10274  sumdmdi 10278  eeeeanv 10372  ntunte 10376  cmpdom 10400  homib 10604

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