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

Theorem ancom 257
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 256 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm3.22 256 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 121 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  ancomd  258  ancomsd  260  pm4.71r  376  pm5.32rd  432  pm5.32ri  436  anbi2ci  440  anbi12ci  442  mpan10  451  an12  503  an32  504  an13  505  an42  529  andir  743  rbaib  841  rbaibr  842  3anrot  901  3ancoma  903  excxor  1285  xorcom  1295  xordc  1299  xordc1  1300  dfbi3dc  1304  ancomsimp  1345  exancom  1515  19.29r  1528  19.42h  1593  19.42  1594  eu1  1941  moaneu  1992  moanmo  1993  2eu7  2010  eq2tri  2115  r19.28av  2466  r19.29r  2468  r19.42v  2484  rexcomf  2489  rabswap  2505  euxfr2dc  2749  rmo4  2757  reu8  2760  rmo3  2877  incom  3157  difin2  3227  symdifxor  3231  inuni  3937  eqvinop  4008  uniuni  4211  dtruex  4311  elvvv  4431  brinxp2  4435  dmuni  4573  dfres2  4686  dfima2  4698  imadmrn  4706  imai  4709  cnvxp  4770  cnvcnvsn  4825  mptpreima  4842  rnco  4855  unixpm  4881  ressn  4886  xpcom  4892  fncnv  4993  fununi  4995  imadiflem  5006  fnres  5043  fnopabg  5050  dff1o2  5159  eqfnfv3  5295  respreima  5323  fsn  5363  fliftcnv  5463  isoini  5485  spc2ed  5882  brtpos2  5897  tpostpos  5910  tposmpt2  5927  nnaord  6113  xpsnen  6326  xpcomco  6331  supmoti  6399  elni2  6470  enq0enq  6587  prltlu  6643  prnmaxl  6644  prnminu  6645  nqprrnd  6699  ltpopr  6751  letri3  7158  lesub0  7548  creur  7987  xrletri3  8822  iooneg  8957  iccneg  8958  elfzuzb  8986  fzrev  9048  redivap  9702  imdivap  9709  rersqreu  9855  lenegsq  9922  climrecvg1n  10098
  Copyright terms: Public domain W3C validator