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

Theorem orc 643
 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 641 . . 3 (((𝜑𝜓) → (𝜑𝜓)) ↔ ((𝜑 → (𝜑𝜓)) ∧ (𝜓 → (𝜑𝜓))))
31, 2mpbi 137 . 2 ((𝜑 → (𝜑𝜓)) ∧ (𝜓 → (𝜑𝜓)))
43simpli 108 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-io 640 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  pm2.67-2  644  pm1.4  656  orci  660  orcd  662  orcs  664  pm2.45  667  biorfi  675  pm1.5  692  pm2.4  705  pm4.44  706  pm4.45  708  pm3.48  709  pm2.76  732  orabs  738  ordi  740  andi  742  pm4.72  747  biort  749  dcim  795  pm2.54dc  801  pm4.78i  819  pm2.85dc  822  dcor  854  pm5.71dc  879  dedlema  887  3mix1  1084  xoranor  1284  19.33  1389  hbor  1454  nford  1475  19.30dc  1534  19.43  1535  19.32r  1586  moor  1987  r19.32r  2474  ssun1  3133  undif3ss  3225  reuun1  3246  prmg  3516  opthpr  3570  issod  4083  elelsuc  4173  ordtri2or2exmidlem  4278  regexmidlem1  4285  nndceq  6107  nndcel  6108  swoord1  6165  swoord2  6166  addlocprlem  6690  msqge0  7680  mulge0  7683  ltleap  7694  nn1m1nn  8007  elnnz  8311  zletric  8345  zlelttric  8346  zmulcl  8354  zdceq  8373  zdcle  8374  zdclt  8375  ltpnf  8802  xrlttri3  8818  fzdcel  9005  qletric  9200  qlelttric  9201  qdceq  9203  nn0o1gt2  10216  bj-nn0suc0  10441
 Copyright terms: Public domain W3C validator