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

Theorem orc 620
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
orc (φ → (φ ψ))

Proof of Theorem orc
StepHypRef Expression
1 id 19 . . 3 ((φ ψ) → (φ ψ))
2 jaob 618 . . 3 (((φ ψ) → (φ ψ)) ↔ ((φ → (φ ψ)) (ψ → (φ ψ))))
31, 2mpbi 133 . 2 ((φ → (φ ψ)) (ψ → (φ ψ)))
43simpli 104 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-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm2.67-2  621  pm1.4  633  orci  637  orcd  639  orcs  641  pm2.45  644  biorfi  652  pm1.5  669  pm2.4  682  pm4.44  683  pm4.45  685  pm3.48  686  pm2.76  708  orabs  714  orabsOLD  715  ordi  717  andi  719  pm4.72  724  biort  726  dcim  772  pm2.54dc  778  pm4.78i  796  pm2.85dc  799  dcor  829  pm5.71dc  854  dedlema  862  3mix1  1059  xoranor  1251  19.33  1349  hbor  1416  nford  1437  19.30dc  1496  19.43  1497  19.32r  1548  moor  1949  r19.32r  2431  ssun1  3079  undif3ss  3171  reuun1  3192  prmg  3459  opthpr  3513  issod  4026  elelsuc  4091  regexmidlem1  4198  nndceq  5986  nndcel  5987  swoord1  6042  swoord2  6043  addlocprlem  6384  bj-nn0suc0  7368
  Copyright terms: Public domain W3C validator