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

Axiom ax-ia2 100
Description: Right 'and' elimination. Axiom 2 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
Assertion
Ref Expression
ax-ia2

Detailed syntax breakdown of Axiom ax-ia2
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wa 97 . 2
43, 2wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  simpr  103  pm5.54dc  815  dcan  828  bilukdc  1268  sbequilem  1697  spsbe  1701  ssddif  3144  difin  3147  peano2  4241  xpmlem  4667  imadiflem  4900  imain  4903  fvelrnb  5142  funfvima3  5313  acexmidlemcase  5427  fnofval  5640  caofinvl  5652  rdgivallem  5884  frecabex  5895  frectfr  5896  frecrdg  5904  oawordi  5960  nnaordi  5988  nnaordex  6007  nnawordex  6008  nnm00  6009  dmaddpqlem  6230  nqpi  6231  ltaddnq  6259  prarloclemarch2  6270  ltrnqg  6271  enq0sym  6281  nqnq0pi  6287  nq0nn  6291  addnq0mo  6296  mulnq0mo  6297  addnnnq0  6298  prloc  6339  prarloclemlt  6341  prarloclemlo  6342  ltdfpr  6354  genplt2i  6358  genpml  6366  aptiprlemu  6468  recexsrlem  6518  reapval  7165  apreap  7176  reapneg  7184  apsym  7190  apcotr  7191  apneg  7195  bj-omtrans  7374
  Copyright terms: Public domain W3C validator