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

Theorem olc 701
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 700 . . 3 (((𝜓𝜑) → (𝜓𝜑)) ↔ ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑))))
31, 2mpbi 144 . 2 ((𝜓 → (𝜓𝜑)) ∧ (𝜑 → (𝜓𝜑)))
43simpri 112 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-io 699
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  oibabs  704  pm1.4  717  olci  722  pm2.07  727  pm2.46  729  biorf  734  pm1.5  755  pm2.41  766  pm4.78i  772  pm3.48  775  ordi  806  andi  808  pm4.72  813  stdcn  833  pm2.54dc  877  pm2.85dc  891  dcor  920  dedlemb  955  xoranor  1359  19.33  1464  hbor  1526  nford  1547  19.30dc  1607  19.43  1608  19.32r  1660  euor2  2064  mooran2  2079  r19.32r  2603  undif3ss  3368  undif4  3456  issod  4279  onsucelsucexmid  4489  sucprcreg  4508  0elnn  4578  acexmidlemph  5817  nntri3or  6440  swoord1  6509  swoord2  6510  exmidaclem  7143  exmidontri2or  7178  addlocprlem  7455  nqprloc  7465  apreap  8462  zletric  9211  zlelttric  9212  zmulcl  9220  zdceq  9239  zdcle  9240  zdclt  9241  nn0lt2  9245  elnn1uz2  9518  mnflt  9690  mnfltpnf  9692  xrltso  9703  fzdcel  9942  fzm1  10002  qletric  10143  qlelttric  10144  qdceq  10146  nn0o1gt2  11796  bj-fadc  13337  decidin  13382  triap  13611  tridceq  13638
  Copyright terms: Public domain W3C validator