Theorem ancom 266

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 265	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 265	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 126	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ancomd  267  ancomsd  269  biancomi  270  biancomd  271  pm4.71r  390  pm5.32rd  451  pm5.32ri  455  anbi2ci  459  anbi12ci  461  bianassc  470  mpan10  474  an12  561  an32  562  an13  563  an42  587  andir  820  rbaib  922  rbaibr  923  3anrot  985  3ancoma  987  excxor  1389  xorcom  1399  xordc  1403  xordc1  1404  dfbi3dc  1408  ancomsimp  1451  exancom  1619  19.29r  1632  19.42h  1698  19.42  1699  eu1  2067  moaneu  2118  moanmo  2119  2eu7  2136  eq2tri  2253  r19.28av  2630  r19.29r  2632  r19.42v  2651  rexcomf  2656  rabswap  2673  euxfr2dc  2945  rmo4  2953  reu8  2956  rmo3f  2957  rmo3  3077  incom  3351  difin2  3421  symdifxor  3425  inuni  4184  eqvinop  4272  uniuni  4482  dtruex  4591  elvvv  4722  brinxp2  4726  dmuni  4872  dfres2  4994  dfima2  5007  imadmrn  5015  imai  5021  cnvxp  5084  cnvcnvsn  5142  mptpreima  5159  rnco  5172  unixpm  5201  ressn  5206  xpcom  5212  fncnv  5320  fununi  5322  imadiflem  5333  fnres  5370  fnopabg  5377  dff1o2  5505  eqfnfv3  5657  respreima  5686  fsn  5730  fliftcnv  5838  isoini  5861  spc2ed  6286  brtpos2  6304  tpostpos  6317  tposmpo  6334  nnaord  6562  pmex  6707  elpmg  6718  mapval2  6732  mapsnen  6865  map1  6866  xpsnen  6875  xpcomco  6880  elfi2  7031  supmoti  7052  cnvti  7078  2omotaplemap  7317  elni2  7374  enq0enq  7491  prltlu  7547  prnmaxl  7548  prnminu  7549  nqprrnd  7603  ltpopr  7655  letri3  8100  lesub0  8498  creur  8978  xrletri3  9870  iooneg  10054  iccneg  10055  elfzuzb  10085  fzrev  10150  redivap  11018  imdivap  11025  rersqreu  11172  lenegsq  11239  climrecvg1n  11491  fisumcom2  11581  fsumcom  11582  fprodcom2fi  11769  fprodcom  11770  gcdcom  12110  bezoutlembi  12142  dfgcd2  12151  lcmcom  12202  isprm2  12255  unennn  12554  dfrhm2  13650  issubrng  13695  ntreq0  14300  restopn2  14351  ismet2  14522  blres  14602  metrest  14674  dedekindicclemicc  14786  sincosq3sgn  14963  lgsdi  15153