ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancom Unicode version

Theorem ancom 264
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
StepHypRef Expression
1 pm3.22 263 . 2  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
2 pm3.22 263 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
31, 2impbii 125 1  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ancomd  265  ancomsd  267  biancomi  268  biancomd  269  pm4.71r  387  pm5.32rd  446  pm5.32ri  450  anbi2ci  454  anbi12ci  456  mpan10  465  an12  550  an32  551  an13  552  an42  576  andir  808  rbaib  906  rbaibr  907  3anrot  967  3ancoma  969  excxor  1356  xorcom  1366  xordc  1370  xordc1  1371  dfbi3dc  1375  ancomsimp  1416  exancom  1587  19.29r  1600  19.42h  1665  19.42  1666  eu1  2022  moaneu  2073  moanmo  2074  2eu7  2091  eq2tri  2197  r19.28av  2566  r19.29r  2568  r19.42v  2586  rexcomf  2591  rabswap  2607  euxfr2dc  2864  rmo4  2872  reu8  2875  rmo3f  2876  rmo3  2995  incom  3263  difin2  3333  symdifxor  3337  inuni  4075  eqvinop  4160  uniuni  4367  dtruex  4469  elvvv  4597  brinxp2  4601  dmuni  4744  dfres2  4866  dfima2  4878  imadmrn  4886  imai  4890  cnvxp  4952  cnvcnvsn  5010  mptpreima  5027  rnco  5040  unixpm  5069  ressn  5074  xpcom  5080  fncnv  5184  fununi  5186  imadiflem  5197  fnres  5234  fnopabg  5241  dff1o2  5365  eqfnfv3  5513  respreima  5541  fsn  5585  fliftcnv  5689  isoini  5712  spc2ed  6123  brtpos2  6141  tpostpos  6154  tposmpo  6171  nnaord  6398  pmex  6540  elpmg  6551  mapval2  6565  mapsnen  6698  map1  6699  xpsnen  6708  xpcomco  6713  elfi2  6853  supmoti  6873  cnvti  6899  elni2  7115  enq0enq  7232  prltlu  7288  prnmaxl  7289  prnminu  7290  nqprrnd  7344  ltpopr  7396  letri3  7838  lesub0  8234  creur  8710  xrletri3  9581  iooneg  9764  iccneg  9765  elfzuzb  9793  fzrev  9857  redivap  10639  imdivap  10646  rersqreu  10793  lenegsq  10860  climrecvg1n  11110  fisumcom2  11200  fsumcom  11201  gcdcom  11651  bezoutlembi  11682  dfgcd2  11691  lcmcom  11734  isprm2  11787  unennn  11899  ntreq0  12290  restopn2  12341  ismet2  12512  blres  12592  metrest  12664  dedekindicclemicc  12768  sincosq3sgn  12898
  Copyright terms: Public domain W3C validator