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

Theorem olc 642
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 641 . . 3 (((𝜓𝜑) → (𝜓𝜑)) ↔ ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑))))
31, 2mpbi 137 . 2 ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑)))
43simpri 110 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm1.4  656  olci  661  pm2.07  666  pm2.46  668  biorf  673  pm1.5  692  pm2.41  703  pm3.48  709  ordi  740  andi  742  pm4.72  747  pm2.54dc  801  oibabs  811  pm4.78i  819  pm2.85dc  822  dcor  854  dedlemb  888  xoranor  1284  19.33  1389  hbor  1454  nford  1475  19.30dc  1534  19.43  1535  19.32r  1586  euor2  1974  mooran2  1989  r19.32r  2474  undif3ss  3226  undif4  3312  issod  4084  onsucelsucexmid  4283  sucprcreg  4301  0elnn  4368  acexmidlemph  5533  nntri3or  6103  swoord1  6166  swoord2  6167  addlocprlem  6691  nqprloc  6701  apreap  7652  zletric  8346  zlelttric  8347  zmulcl  8355  zdceq  8374  zdcle  8375  zdclt  8376  nn0lt2  8380  elnn1uz2  8641  mnflt  8805  mnfltpnf  8807  xrltso  8818  fzdcel  9006  fzm1  9064  qletric  9201  qlelttric  9202  qdceq  9204  nn0o1gt2  10217
  Copyright terms: Public domain W3C validator