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

Theorem ancom 262
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 261 . 2  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
2 pm3.22 261 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
31, 2impbii 124 1  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ancomd  263  ancomsd  265  pm4.71r  382  pm5.32rd  439  pm5.32ri  443  anbi2ci  447  anbi12ci  449  mpan10  458  an12  526  an32  527  an13  528  an42  552  andir  766  rbaib  866  rbaibr  867  3anrot  927  3ancoma  929  excxor  1312  xorcom  1322  xordc  1326  xordc1  1327  dfbi3dc  1331  ancomsimp  1372  exancom  1542  19.29r  1555  19.42h  1620  19.42  1621  eu1  1970  moaneu  2021  moanmo  2022  2eu7  2039  eq2tri  2144  r19.28av  2501  r19.29r  2503  r19.42v  2520  rexcomf  2525  rabswap  2541  euxfr2dc  2791  rmo4  2799  reu8  2802  rmo3  2919  incom  3181  difin2  3250  symdifxor  3254  inuni  3965  eqvinop  4043  uniuni  4246  dtruex  4347  elvvv  4468  brinxp2  4472  dmuni  4613  dfres2  4728  dfima2  4740  imadmrn  4748  imai  4752  cnvxp  4813  cnvcnvsn  4870  mptpreima  4887  rnco  4900  unixpm  4929  ressn  4934  xpcom  4940  fncnv  5042  fununi  5044  imadiflem  5055  fnres  5092  fnopabg  5099  dff1o2  5215  eqfnfv3  5356  respreima  5384  fsn  5426  fliftcnv  5529  isoini  5552  spc2ed  5949  brtpos2  5964  tpostpos  5977  tposmpt2  5994  nnaord  6214  pmex  6356  elpmg  6367  mapval2  6381  mapsnen  6474  map1  6475  xpsnen  6483  xpcomco  6488  supmoti  6625  cnvti  6651  elni2  6810  enq0enq  6927  prltlu  6983  prnmaxl  6984  prnminu  6985  nqprrnd  7039  ltpopr  7091  letri3  7503  lesub0  7894  creur  8347  xrletri3  9195  iooneg  9330  iccneg  9331  elfzuzb  9359  fzrev  9421  redivap  10196  imdivap  10203  rersqreu  10349  lenegsq  10416  climrecvg1n  10620  gcdcom  10832  bezoutlembi  10861  dfgcd2  10870  lcmcom  10913  isprm2  10966  unennn  11077
  Copyright terms: Public domain W3C validator