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

Theorem olc 632
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 631 . . 3 (((𝜓𝜑) → (𝜓𝜑)) ↔ ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑))))
31, 2mpbi 133 . 2 ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑)))
43simpri 106 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm1.4  646  olci  651  pm2.07  656  pm2.46  658  biorf  663  pm1.5  682  pm2.41  693  pm3.48  699  ordi  729  andi  731  pm4.72  736  pm2.54dc  790  oibabs  800  pm4.78i  808  pm2.85dc  811  dcor  843  dedlemb  877  xoranor  1268  19.33  1373  hbor  1438  nford  1459  19.30dc  1518  19.43  1519  19.32r  1570  euor2  1958  mooran2  1973  r19.32r  2457  undif3ss  3198  undif4  3284  issod  4056  onsucelsucexmid  4255  sucprcreg  4273  0elnn  4340  acexmidlemph  5505  nntri3or  6072  swoord1  6135  swoord2  6136  addlocprlem  6633  nqprloc  6643  apreap  7578  zletric  8289  zlelttric  8290  zmulcl  8297  zdceq  8316  zdcle  8317  zdclt  8318  nn0lt2  8322  elnn1uz2  8544  mnflt  8704  mnfltpnf  8706  xrltso  8717  fzdcel  8904  fzm1  8962  qletric  9099  qlelttric  9100  qdceq  9102
  Copyright terms: Public domain W3C validator