ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancom GIF 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 ((𝜑𝜓) ↔ (𝜓𝜑))

Proof of Theorem ancom
StepHypRef Expression
1 pm3.22 261 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm3.22 261 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 124 1 ((𝜑𝜓) ↔ (𝜓𝜑))
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  3966  eqvinop  4044  uniuni  4247  dtruex  4348  elvvv  4469  brinxp2  4473  dmuni  4614  dfres2  4731  dfima2  4743  imadmrn  4751  imai  4755  cnvxp  4816  cnvcnvsn  4873  mptpreima  4890  rnco  4903  unixpm  4932  ressn  4937  xpcom  4943  fncnv  5045  fununi  5047  imadiflem  5058  fnres  5095  fnopabg  5102  dff1o2  5221  eqfnfv3  5362  respreima  5390  fsn  5432  fliftcnv  5535  isoini  5558  spc2ed  5955  brtpos2  5970  tpostpos  5983  tposmpt2  6000  nnaord  6220  pmex  6362  elpmg  6373  mapval2  6387  mapsnen  6480  map1  6481  xpsnen  6489  xpcomco  6494  supmoti  6632  cnvti  6658  elni2  6817  enq0enq  6934  prltlu  6990  prnmaxl  6991  prnminu  6992  nqprrnd  7046  ltpopr  7098  letri3  7510  lesub0  7901  creur  8354  xrletri3  9202  iooneg  9337  iccneg  9338  elfzuzb  9366  fzrev  9428  redivap  10204  imdivap  10211  rersqreu  10357  lenegsq  10424  climrecvg1n  10629  gcdcom  10847  bezoutlembi  10876  dfgcd2  10885  lcmcom  10928  isprm2  10981  unennn  11092
  Copyright terms: Public domain W3C validator