Theorem ancom 437

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 438  ancomsd 439  pm3.22 440  anbi1i 483  an12 486  an23 487  anabs5 495  an42 509  bicom 522  andir 607  anbi1d 619  pm4.71r 638  pm5.32ri 648  pm5.32rd 650  xor 673  xor2 675  biantrurd 729  consensus 769  rnlem 775  3anrot 782  3ancoma 784  exancom 1056  19.29r 1074  19.42 1098  exan 1108  eu1 1394  mooran1 1427  moaneu 1432  moanmo 1433  2eu3 1454  2eu6 1457  2eu7 1458  2eu8 1459  eq2tr 1536  clabel 1585  r19.28av 1758  r19.29r 1760  r19.42v 1767  rabswap 1774  ralcom 1777  rexcom 1778  gencbvex 1841  euxfr2 1929  rmo4 1936  reu8 1939  incom 2211  symdif2 2269  difin0ss 2336  iunid 2607  moabex 2772  eqvinop 2797  dfid3 2842  uniuni 2886  reuxfr2 2909  ordtri4 2990  ordpwsuc 3072  elxp2 3209  cnvco 3306  dmuni 3325  dfima2 3411  imadmrn 3420  imai 3423  asymref 3445  intirr 3447  cnvsn 3455  rnuni 3465  cnvxp 3470  rninxp 3488  cores 3505  rnco 3508  cnvpo 3528  fncnv 3567  fununi 3569  funin 3572  f1cnv 3672  tz6.12-1 3742  fsn 3840  isoini 3906  tfrlem7 3923  ndmoprcom 4053  2ndconst 4103  oaord 4187  pmex 4333  mapval2 4341  mapsnen 4435  map1 4436  xpsnen 4441  xpcomen 4445  pw2en 4452  mapxpen 4501  cp 4732  aceq5lem1 4745  aceq5lem2 4746  aceq5lem3 4747  aceq6b 4752  kmlem3 4777  brdom7disj 4814  brdom6disj 4815  cf0 4922  genpass 5124  1pr 5129  addcompr 5135  mulcompr 5137  reclem2pr 5169  elreal 5262  ltxrt 5507  letri3t 5529  lesub0 5624  addgtge0t 5661  divmul13t 5784  divmul24t 5785  divdivdivt 5787  ioonegt 6407  iccnegt 6408  icounlem 6413  indstr 6462  elfzuzb 6477  elfzuz2t 6487  fzrevt 6512  lenegsqt 6885  cau5 6919  sumex 6981  clm4 7080  sinbndt 7466  cosbndt 7467  infpn2 7510  infxpidmlem9 7561  istps3 7609  tgval3t 7624  tgss3t 7637  clsval2 7682  metxp 7831  issubg 8112  sincosq1sgn 8699  sincosq2sgn 8700  sincosq3sgn 8701  sincosq4sgn 8702  h2hcau 8844  shorth 9163  5oalem2 9595  3oalem2 9603  mdsldmd1 10253  chrelat 10286  cvexchlem 10290  mdsymlem8 10332  sumdmdi 10337  eeeeanv 10431  ntunte 10434  cmpdom 10458  rcfpfillem3 10565  homib 10695

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