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

Theorem olc 619
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 618 . . 3 (((ψ φ) → (ψ φ)) ↔ ((ψ → (ψ φ)) (φ → (ψ φ))))
31, 2mpbi 133 . 2 ((ψ → (ψ φ)) (φ → (ψ φ)))
43simpri 106 1 (φ → (ψ φ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 616
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm1.4  633  olci  638  pm2.07  643  pm2.46  645  biorf  650  pm1.5  669  pm2.41  680  pm3.48  686  ordi  717  andi  719  pm4.72  724  pm2.54dc  783  oibabs  793  pm4.78i  801  pm2.85dc  804  dcor  831  dedlemb  865  xoranor  1253  19.33  1353  hbor  1420  nford  1441  19.30dc  1500  19.43  1501  19.32r  1552  euor2  1940  mooran2  1955  r19.32r  2435  undif3ss  3175  undif4  3261  issod  4030  onsucelsucexmid  4199  sucprcreg  4211  0elnn  4267  acexmidlemph  5429  nntri3or  5987  swoord1  6046  swoord2  6047  addlocprlem  6390  nqprloc  6400
  Copyright terms: Public domain W3C validator