Theorem ancom 482

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		simpr 350	. . 3 |- ((ph /\ ps) -> ps)
2		simpl 346	. . 3 |- ((ph /\ ps) -> ph)
3	1, 2	jca 310	. 2 |- ((ph /\ ps) -> (ps /\ ph))
4		simpr 350	. . 3 |- ((ps /\ ph) -> ph)
5		simpl 346	. . 3 |- ((ps /\ ph) -> ps)
6	4, 5	jca 310	. 2 |- ((ps /\ ph) -> (ph /\ ps))
7	3, 6	impbii 174	1 |- ((ph /\ ps) <-> (ps /\ ph))

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  ancomd 483  ancoms 484  ancomsd 485  pm3.22 486  anbi1i 539  an12 542  an23 543  anabs5 551  an42 565  bicom 579  andir 666  anbi1d 679  pm4.71r 698  pm5.32ri 708  pm5.32rd 710  xor 734  xor2 736  biantrurdOLD 797  consensusOLD 845  rnlemOLD 854  3anrot 863  3ancoma 865  ancomsimp 1291  exancom 1401  19.29r 1423  19.42 1450  exanOLD 1464  eu1 1786  mooran1OLD 1823  moaneu 1830  moanmo 1831  2eu3 1855  2eu6 1858  2eu7 1859  2eu8 1860  eq2tri 1956  clabel 2014  r19.28av 2226  r19.29r 2229  r19.42v 2237  ralcom 2242  rexcom 2243  rabswap 2256  gencbvexOLD 2335  euxfr2 2437  euind 2439  rmo4 2445  reu8 2448  reuind 2450  incom 2787  symdif2OLD 2858  difin0ss 2939  inuni 3470  moabex 3513  eqvinop 3536  opelopabsb 3564  dfid3 3587  ordtri4OLD 3700  uniuni 3806  reuxfr2d 3844  reuxfr2 3845  ordpwsuc 3896  elxp2 4019  elvvv 4054  cnvcoOLD 4146  dmuni 4166  opres 4225  dfima2 4265  dfima2OLD 4266  imadmrn 4277  imai 4280  asymref 4308  asymrefOLD 4309  asymref2 4310  intirrOLD 4313  rnuni 4327  cnvxp 4332  cnvxpOLD 4333  rninxpOLD 4356  cnvsn 4373  coresOLD 4401  rnco 4404  cnvpo 4427  fncnv 4479  fununi 4481  funinOLD 4485  f1cnv 4611  dff1o2 4639  tz6.12-1 4693  eqfnfv3 4769  fsn 4807  isoini 4877  ndmoprcom 4980  fparlem1 5081  fparlem2 5082  fsplit 5086  reiota4 5107  tfrlem7 5125  oaord 5228  uniqs 5354  pmex 5386  mapval2 5394  mapsnen 5488  map1 5489  xpsnen 5494  xpcomen 5498  pw2en 5505  ordiso 5683  cp 5852  aceq5lem1 5897  aceq5lem2 5898  aceq5lem3 5899  aceq6b 5904  kmlem3 5929  brdom7disj 5966  brdom6disj 5967  cf0 6058  genpass 6264  1pr 6269  addcompr 6275  mulcompr 6277  reclem2pr 6309  elreal 6402  ltxr 6664  letri3 6687  lesub0i 6792  lesub0iOLD 6793  addgtge0OLD 6836  iooneg 7575  iccneg 7576  icounlem 7581  indstr 7630  elfzuzb 7646  elfzuz2 7656  fzrev 7689  lenegsq 8137  cau5i 8171  sumex 8241  clm4i 8340  infpn2 8778  infxpidmlem9 8829  istps3 8877  tgval3 8895  tgss3 8908  clsval2 8961  metxp 9111  issubg 9425  sincosq1sgn 10053  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  exidu1 10373  grpmnd 10393  h2hcau 10481  shorth 10801  5oalem2 11235  3oalem2 11243  mdsldmd1i 11903  chrelati 11936  cvexchlem 11940  mdsymlem8 11982  sumdmdii 11987  bnj170OLD 12035  bnj171OLD 12037  bnj172OLD 12039  bnj173OLD 12041  bnj174OLD 12043  bnj176OLD 12046  bnj177 12047  bnj178 12048  bnj179OLD 12050  bnj182 12053  bnj184OLD 12055  bnj186 12056  bnj257 12096  bnj345OLD 12188  bnj367OLD 12211  bnj32OLD 12399  bnj50OLD 12425  bnj112 12457  bnj134 12478  bnj163OLD 12490  bnj876 12803  bnj878 12805  bnj1370 13094  imim21b 13597  divalglem10 13705  gcdcom 13726  mulgcdlem2 13757  isprm2 13775  dffr5 13831  tz6.26 13913  wfi 13915  frind 13939  soxp 13950  wfrlem5 13961  tfrALTlem 13976  nocvxmin 14029  axfelem14 14044  eeeeanv 14272  excxor 14280  cmpdom 14481  prodex 14656  rcfpfillem3 14930  letri31 15019  homib 15145  settrcon 15247  trer 15361  fictb 15371  ordisoOLD 15374  is1stc3 15469  ist0-2 15539  difin2 15676  respreima 15684  eqfnfv3OLD 15721  fzsplit 15792  fzm1 15796  sstotbnd 15936  heiborlem1 15955  exidresid 16032  isdivrng3 16112  isdmn3 16222  an43OLD 16236  prtlem70 16238  prtlem90 16246  prter1 16282  ancomsimpVD 16689  strdif 16719  posgelem 16795  hlrelat1 17049  pmapglb 17252  polval2 17319

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 164  df-an 242

Copyright terms: Public domain