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 520  andir 605  anbi1d 617  pm4.71r 636  pm5.32ri 646  pm5.32rd 648  xor 671  xor2 673  biantrurd 727  consensus 767  rnlem 773  3anrot 780  3ancoma 782  exancom 1054  19.29r 1072  19.42 1096  exan 1106  eu1 1392  mooran1 1425  moaneu 1430  moanmo 1431  2eu3 1451  2eu6 1454  2eu7 1455  2eu8 1456  eq2tr 1533  clabel 1582  r19.28av 1755  r19.29r 1757  r19.42v 1764  rabswap 1771  ralcom 1774  rexcom 1775  gencbvex 1838  euxfr2 1926  rmo4 1933  reu8 1936  incom 2208  symdif2 2266  difin0ss 2332  iunid 2603  moabex 2766  eqvinop 2791  dfid3 2836  uniuni 2880  reuxfr2 2903  ordtri4 2984  ordpwsuc 3066  elxp2 3203  cnvco 3300  dmuni 3319  dfima2 3405  imadmrn 3414  imai 3417  asymref 3439  intirr 3441  cnvsn 3449  rnuni 3459  cnvxp 3464  rninxp 3482  cores 3499  rnco 3502  cnvpo 3522  fncnv 3561  fununi 3563  funin 3566  f1cnv 3666  tz6.12-1 3736  fsn 3834  isoini 3900  tfrlem7 3917  ndmoprcom 4047  2ndconst 4097  oaord 4181  pmex 4327  mapval2 4335  mapsnen 4429  map1 4430  xpsnen 4435  xpcomen 4439  pw2en 4446  mapxpen 4495  cp 4722  aceq5lem1 4735  aceq5lem2 4736  aceq5lem3 4737  aceq6b 4742  kmlem3 4767  brdom7disj 4804  brdom6disj 4805  cf0 4910  genpass 5112  1pr 5117  addcompr 5123  mulcompr 5125  reclem2pr 5157  elreal 5250  ltxrt 5495  letri3t 5517  lesub0 5612  addgtge0t 5649  divmul13t 5782  divmul24t 5783  divdivdivt 5785  ioonegt 6406  iccnegt 6407  icounlem 6412  indstr 6461  elfzuzb 6476  elfzuz2t 6486  fzrevt 6511  lenegsqt 6885  cau5 6919  sumex 6981  clm4 7080  sinbndt 7465  cosbndt 7466  infpn2 7509  infxpidmlem9 7560  istps3 7608  tgval3t 7625  tgss3t 7638  clsval2 7685  metxp 7834  issubg 8116  sincosq1sgn 8704  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  h2hcau 8849  shorth 9168  5oalem2 9600  3oalem2 9608  mdsldmd1 10258  chrelat 10291  cvexchlem 10295  mdsymlem8 10337  sumdmdi 10342  eeeeanv 10436  ntunte 10439  cmpdom 10468  rcfpfillem3 10589  rcfpfillem3OLD 10590  homib 10724

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