Theorem ancom 263

Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)

Assertion

Ref	Expression
ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		pm3.22 262	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 262	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 125	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ancomd  264  ancomsd  266  pm4.71r  383  pm5.32rd  440  pm5.32ri  444  anbi2ci  448  anbi12ci  450  mpan10  459  an12  529  an32  530  an13  531  an42  555  andir  769  rbaib  869  rbaibr  870  3anrot  930  3ancoma  932  excxor  1315  xorcom  1325  xordc  1329  xordc1  1330  dfbi3dc  1334  ancomsimp  1375  exancom  1545  19.29r  1558  19.42h  1623  19.42  1624  eu1  1974  moaneu  2025  moanmo  2026  2eu7  2043  eq2tri  2148  r19.28av  2506  r19.29r  2508  r19.42v  2525  rexcomf  2530  rabswap  2546  euxfr2dc  2801  rmo4  2809  reu8  2812  rmo3f  2813  rmo3  2931  incom  3193  difin2  3262  symdifxor  3266  inuni  3997  eqvinop  4079  uniuni  4286  dtruex  4388  elvvv  4514  brinxp2  4518  dmuni  4659  dfres2  4777  dfima2  4789  imadmrn  4797  imai  4801  cnvxp  4863  cnvcnvsn  4920  mptpreima  4937  rnco  4950  unixpm  4979  ressn  4984  xpcom  4990  fncnv  5093  fununi  5095  imadiflem  5106  fnres  5143  fnopabg  5150  dff1o2  5271  eqfnfv3  5413  respreima  5441  fsn  5483  fliftcnv  5588  isoini  5611  spc2ed  6012  brtpos2  6030  tpostpos  6043  tposmpt2  6060  nnaord  6282  pmex  6424  elpmg  6435  mapval2  6449  mapsnen  6582  map1  6583  xpsnen  6591  xpcomco  6596  supmoti  6742  cnvti  6768  elni2  6934  enq0enq  7051  prltlu  7107  prnmaxl  7108  prnminu  7109  nqprrnd  7163  ltpopr  7215  letri3  7627  lesub0  8018  creur  8480  xrletri3  9331  iooneg  9466  iccneg  9467  elfzuzb  9495  fzrev  9559  redivap  10369  imdivap  10376  rersqreu  10522  lenegsq  10589  climrecvg1n  10798  fisumcom2  10893  fsumcom  10894  gcdcom  11304  bezoutlembi  11333  dfgcd2  11342  lcmcom  11385  isprm2  11438  unennn  11549  ntreq0  11893