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

Theorem olc 711
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
olc (𝜑 → (𝜓𝜑))

Proof of Theorem olc
StepHypRef Expression
1 id 19 . . 3 ((𝜓𝜑) → (𝜓𝜑))
2 jaob 710 . . 3 (((𝜓𝜑) → (𝜓𝜑)) ↔ ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑))))
31, 2mpbi 145 . 2 ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑)))
43simpri 113 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  oibabs  714  pm1.4  727  olci  732  pm2.07  737  pm2.46  739  biorf  744  pm1.5  765  pm2.41  776  pm4.78i  782  pm3.48  785  ordi  816  andi  818  pm4.72  827  stdcn  847  pm2.54dc  891  pm2.85dc  905  dcor  935  dedlemb  970  xoranor  1377  19.33  1484  hbor  1546  nford  1567  19.30dc  1627  19.43  1628  19.32r  1680  euor2  2084  mooran2  2099  r19.32r  2623  undif3ss  3398  undif4  3487  issod  4321  onsucelsucexmid  4531  sucprcreg  4550  0elnn  4620  acexmidlemph  5871  nntri3or  6497  swoord1  6567  swoord2  6568  exmidaclem  7210  exmidontri2or  7245  addlocprlem  7537  nqprloc  7547  apreap  8547  zletric  9300  zlelttric  9301  zmulcl  9309  zdceq  9331  zdcle  9332  zdclt  9333  nn0lt2  9337  elnn1uz2  9610  mnflt  9786  mnfltpnf  9788  xrltso  9799  fzdcel  10043  fzm1  10103  qletric  10247  qlelttric  10248  qdceq  10250  qsqeqor  10634  nn0o1gt2  11913  prm23lt5  12266  bj-fadc  14694  decidin  14737  triap  14966  tridceq  14993
  Copyright terms: Public domain W3C validator