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

Theorem olc 665
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 664 . . 3 (((𝜓𝜑) → (𝜓𝜑)) ↔ ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑))))
31, 2mpbi 143 . 2 ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑)))
43simpri 111 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm1.4  679  olci  684  pm2.07  689  pm2.46  691  biorf  696  pm1.5  715  pm2.41  726  pm3.48  732  ordi  763  andi  765  pm4.72  770  pm2.54dc  826  oibabs  836  pm4.78i  844  pm2.85dc  847  dcor  879  dedlemb  914  xoranor  1311  19.33  1416  hbor  1481  nford  1502  19.30dc  1561  19.43  1562  19.32r  1613  euor2  2003  mooran2  2018  r19.32r  2510  undif3ss  3249  undif4  3333  issod  4122  onsucelsucexmid  4321  sucprcreg  4340  0elnn  4407  acexmidlemph  5608  nntri3or  6210  swoord1  6275  swoord2  6276  addlocprlem  7041  nqprloc  7051  apreap  8008  zletric  8730  zlelttric  8731  zmulcl  8739  zdceq  8758  zdcle  8759  zdclt  8760  nn0lt2  8764  elnn1uz2  9029  mnflt  9188  mnfltpnf  9190  xrltso  9201  fzdcel  9389  fzm1  9447  qletric  9586  qlelttric  9587  qdceq  9589  nn0o1gt2  10830  decidin  11185
  Copyright terms: Public domain W3C validator