ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-ia1 Structured version   Unicode version

Axiom ax-ia1 99
Description: Left 'and' elimination. Axiom 1 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
Assertion
Ref Expression
ax-ia1

Detailed syntax breakdown of Axiom ax-ia1
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wa 97 . 2
43, 1wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  simpl  102  pm5.54dc  815  dcan  828  pm4.42r  864  xordc1  1265  anxordi  1272  falantru  1275  sbcof2  1669  sbequilem  1697  sbequ8  1705  rexim  2387  mosubt  2691  difdif  3042  indifdir  3166  rexm  3295  opelopabsb  3967  ordelord  4063  ordtriexmidlem  4188  tfi  4228  peano1  4240  peano2  4241  mosubopt  4328  imadiflem  4900  funimaexg  4905  fvelrnb  5142  acexmidlemcase  5427  brtpos2  5784  frectfr  5896  omv2  5956  omsuc  5962  nnsucelsuc  5981  nnaordi  5988  nnm00  6009  ecexr  6018  dmaddpqlem  6230  ltaddnq  6259  ltbtwnnqq  6266  ltrnqg  6271  enq0sym  6281  addnq0mo  6296  mulnq0mo  6297  addnnnq0  6298  prarloclemn  6347  prarloc  6351  ltdfpr  6354  genplt2i  6358  reapval  7165  reapneg  7184  bj-omtrans  7374  bj-inf2vnlem1  7384
  Copyright terms: Public domain W3C validator