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  563  an32  564  an13  565  an42  589  andir  827  rbaib  929  rbaibr  930  ifptru  998  ifpfal  999  3anrot  1010  3ancoma  1012  excxor  1423  xorcom  1433  xordc  1437  xordc1  1438  dfbi3dc  1442  ancomsimp  1486  exancom  1657  19.29r  1670  19.42h  1735  19.42  1736  eu1  2107  moaneu  2159  moanmo  2160  2eu7  2177  eq2tri  2294  r19.28av  2681  r19.29r  2683  r19.42v  2702  rexcomf  2707  rabswap  2725  euxfr2dc  3005  rmo4  3013  reu8  3016  rmo3f  3017  rmo3  3138  incom  3415  difin2  3487  symdifxor  3491  elif  3638  inuni  4272  eqvinop  4364  uniuni  4577  dtruex  4686  elvvv  4818  brinxp2  4822  dmuni  4971  dfres2  5095  dfima2  5108  imadmrn  5116  imai  5123  cnvxp  5186  cnvcnvsn  5244  mptpreima  5261  rnco  5274  unixpm  5303  ressn  5308  xpcom  5314  fncnv  5427  fununi  5429  imadiflem  5440  fnres  5480  fnopabg  5487  dff1o2  5624  eqfnfv3  5782  respreima  5810  fsn  5854  fliftcnv  5974  isoini  5997  spc2ed  6442  brtpos2  6495  tpostpos  6508  tposmpo  6525  nnaord  6755  pmex  6900  elpmg  6911  mapval2  6925  mapsnend  7065  mapsnen  7066  map1  7067  xpsnen  7085  xpcomco  7090  elfi2  7272  supmoti  7297  cnvti  7323  2omotaplemap  7587  elni2  7645  enq0enq  7762  prltlu  7818  prnmaxl  7819  prnminu  7820  nqprrnd  7874  ltpopr  7926  letri3  8370  lesub0  8770  creur  9250  xrletri3  10156  iooneg  10340  iccneg  10341  elfzuzb  10372  fzrev  10440  redivap  11584  imdivap  11591  rersqreu  11738  lenegsq  11805  climrecvg1n  12058  fisumcom2  12149  fsumcom  12150  fprodcom2fi  12337  fprodcom  12338  gcdcom  12694  bezoutlembi  12726  dfgcd2  12735  lcmcom  12786  isprm2  12839  ballotfilem2  13172  unennn  13232  dfrhm2  14399  issubrng  14445  ntreq0  15123  restopn2  15174  ismet2  15345  blres  15425  metrest  15497  dedekindicclemicc  15623  sincosq3sgn  15819  lgsdi  16036  lgsquadlem3  16078  2lgslem1a  16087  clwwlkn1  16539  clwwlkn2  16542  iseupthf1o  16569  eupth2lem2dc  16580