Theorem ancom 333

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 260	. . 3 |- ((ph /\ ps) -> ps)
2		pm3.26 256	. . 3 |- ((ph /\ ps) -> ph)
3	1, 2	jca 236	. 2 |- ((ph /\ ps) -> (ps /\ ph))
4		pm3.27 260	. . 3 |- ((ps /\ ph) -> ph)
5		pm3.26 256	. . 3 |- ((ps /\ ph) -> ps)
6	4, 5	jca 236	. 2 |- ((ps /\ ph) -> (ph /\ ps))
7	3, 6	impbi 139	1 |- ((ph /\ ps) <-> (ps /\ ph))

Syntax hints:   <-> wb 127   /\ wa 196

This theorem is referenced by:  ancoms 334  ancomsd 335  anbi1i 368  an12 370  an23 371  anabs5 375  an42 389  bicom 398  andir 457  anbi1d 469  pm4.71r 482  pm5.32ri 490  pm5.32rd 492  xor 500  biass 511  biantrurd 546  consensus 574  rnlem 579  3anrot 586  3ancoma 588  exancom 736  19.29r 753  19.42 775  exan 784  eu1 1019  mooran1 1049  eupickb 1056  2eu3 1069  cleq2tr 1148  r19.28av 1294  r19.29r 1296  r19.42v 1303  ralcom 1312  rexcom 1313  gencbvex 1372  euxfr2 1435  reuxfr2 1579  incom 1636  symdif2 1690  difin0ss 1753  moabex 1868  eqvinop 1901  ordtri4 2235  onpwsuc 2315  elxp2 2443  brinxp 2466  cnvco 2520  dmuni 2538  dfima2 2604  imadmrn 2610  imai 2613  intirr 2628  cnvsn 2636  rnuni 2646  cnvxp 2651  cores 2659  dmco2 2673  fununi 2705  funin 2708  f1cnv 2782  tz6.12-1 2842  fsn 2895  isoini 2938  isowe 2941  tfrlem7 2955  ndmoprcom 3061  oaord 3149  nnmord 3189  mapsnen 3334  map1 3335  xpsnen 3339  xpcomen 3343  pw2en 3348  mapxpen 3390  cp 3547  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  aceq6b 3565  kmlem3 3582  cf0 3705  genpass 3906  1pr 3911  addcompr 3917  mulcompr 3919  reclem2pr 3951  elreal 4044  divdivdivt 4265  letri3t 4283  lesub0 4341  uzwo2 4606  indstr 4611  znnen 4930  infxpidmlem9 4941  shorth 5176  5oalem2 5545  3oalem2 5553  chrelat 5757  cvexchlem 5759  mdsymlem8 5783  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org