Theorem ancom 446

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 330	. . 3 |- ((ph /\ ps) -> ps)
2		pm3.26 326	. . 3 |- ((ph /\ ps) -> ph)
3	1, 2	jca 295	. 2 |- ((ph /\ ps) -> (ps /\ ph))
4		pm3.27 330	. . 3 |- ((ps /\ ph) -> ph)
5		pm3.26 326	. . 3 |- ((ps /\ ph) -> ps)
6	4, 5	jca 295	. 2 |- ((ps /\ ph) -> (ph /\ ps))
7	3, 6	impbii 164	1 |- ((ph /\ ps) <-> (ps /\ ph))

Syntax hints:   <-> wb 153   /\ wa 230

This theorem is referenced by:  ancoms 447  ancomsd 448  pm3.22 449  anbi1i 492  an12 495  an23 496  anabs5 504  an42 518  bicom 531  andir 616  anbi1d 628  pm4.71r 647  pm5.32ri 657  pm5.32rd 659  xor 682  xor2 684  biantrurd 739  consensus 779  rnlem 785  3anrot 792  3ancoma 794  exancom 1095  19.29r 1113  19.42 1137  exan 1147  eu1 1434  mooran1 1467  moaneu 1472  moanmo 1473  2eu3 1494  2eu6 1497  2eu7 1498  2eu8 1499  eq2tri 1580  clabel 1629  r19.28av 1802  r19.29r 1804  r19.42v 1811  rabswap 1818  ralcom 1821  rexcom 1822  gencbvex 1885  euxfr2 1973  rmo4 1980  reu8 1983  incom 2259  symdif2 2317  difin0ss 2384  iunid 2657  moabex 2822  eqvinop 2847  dfid3 2892  uniuni 2937  reuxfr2 2960  ordtri4 3041  ordpwsuc 3123  elxp2 3260  cnvco 3357  dmuni 3376  dfima2 3462  imadmrn 3471  imai 3474  asymref 3496  intirr 3498  cnvsn 3506  rnuni 3516  cnvxp 3521  rninxp 3539  cores 3556  rnco 3559  cnvpo 3579  fncnv 3618  fununi 3620  funin 3623  f1cnv 3723  tz6.12-1 3793  fsn 3891  isoini 3958  tfrlem7 3975  ndmoprcom 4105  2ndconst 4155  oaord 4239  uniqs 4356  pmex 4388  mapval2 4396  mapsnen 4490  map1 4491  xpsnen 4498  xpcomen 4502  pw2en 4509  mapxpen 4560  cp 4784  aceq5lem1 4797  aceq5lem2 4798  aceq5lem3 4799  aceq6b 4804  kmlem3 4829  brdom7disj 4866  brdom6disj 4867  cf0 4975  genpass 5177  1pr 5182  addcompr 5188  mulcompr 5190  reclem2pr 5222  elreal 5315  ltxr 5560  letri3 5582  lesub0i 5677  addgtge0 5714  divmul13 5840  divmul24 5841  divdivdiv 5843  iooneg 6432  iccneg 6433  icounlem 6438  indstr 6487  elfzuzb 6502  elfzuz2 6512  fzrev 6537  lenegsq 6975  cau5i 7009  sumex 7071  clm4i 7170  sinbnd 7557  cosbnd 7558  infpn2 7601  infxpidmlem9 7652  istps3 7699  tgval3 7714  tgss3 7727  clsval2 7770  metxp 7919  issubg 8200  sincosq1sgn 8787  sincosq2sgn 8788  sincosq3sgn 8789  sincosq4sgn 8790  h2hcau 8932  shorth 9251  5oalem2 9683  3oalem2 9691  mdsldmd1i 10342  chrelati 10375  cvexchlem 10379  mdsymlem8 10421  sumdmdii 10426  eeeeanv 10522  ntunte 10525  cmpdom 10549  rcfpfillem3 10673  homib 10806

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 154  df-an 232

Copyright terms: Public domain