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

Theorem ancom 253
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 252 . 2 ((φ ψ) → (ψ φ))
2 pm3.22 252 . 2 ((ψ φ) → (φ ψ))
31, 2impbii 117 1 ((φ ψ) ↔ (ψ φ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ancomd  254  ancomsd  256  pm4.71r  370  pm5.32rd  427  pm5.32ri  431  anbi2ci  435  anbi12ci  437  mpan10  446  an12  483  an32  484  an13  485  an42  508  andir  720  rbaib  818  rbaibr  819  3anrot  876  3ancoma  878  excxor  1252  xorcom  1260  xordc  1264  xordc1  1265  dfbi3dc  1269  ancomsimp  1305  exancom  1477  19.29r  1490  19.42h  1555  19.42  1556  eu1  1903  moaneu  1954  moanmo  1955  2eu7  1972  eq2tri  2077  r19.28av  2423  r19.29r  2425  r19.42v  2441  rexcomf  2446  rabswap  2462  euxfr2dc  2699  rmo4  2707  reu8  2710  rmo3  2822  incom  3102  difin2  3172  symdifxor  3176  inuni  3879  eqvinop  3950  uniuni  4129  dtruex  4217  elvvv  4326  brinxp2  4330  dmuni  4468  dfres2  4581  dfima2  4593  imadmrn  4601  imai  4604  cnvxp  4665  cnvcnvsn  4720  mptpreima  4737  rnco  4750  unixpm  4776  ressn  4781  xpcom  4787  fncnv  4887  fununi  4889  imadiflem  4900  fnres  4937  fnopabg  4944  dff1o2  5052  eqfnfv3  5188  respreima  5216  fsn  5256  fliftcnv  5356  isoini  5378  brtpos2  5784  tpostpos  5797  tposmpt2  5814  nnaord  5989  elni2  6168  enq0enq  6280  prltlu  6335  prnmaxl  6336  prnminu  6337  nqprrnd  6392  ltpopr  6426
  Copyright terms: Public domain W3C validator