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

Theorem orc 684
 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 682 . . 3 (((𝜑𝜓) → (𝜑𝜓)) ↔ ((𝜑 → (𝜑𝜓)) ∧ (𝜓 → (𝜑𝜓))))
31, 2mpbi 144 . 2 ((𝜑 → (𝜑𝜓)) ∧ (𝜓 → (𝜑𝜓)))
43simpli 110 1 (𝜑 → (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 680 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 681 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm2.67-2  685  pm1.4  699  orci  703  orcd  705  orcs  707  pm2.45  710  biorfi  718  pm1.5  737  pm2.4  750  pm4.44  751  pm4.78i  754  pm4.45  756  pm3.48  757  pm2.76  780  orabs  786  ordi  788  andi  790  pm4.72  795  biort  797  dcim  809  pm2.54dc  859  pm2.85dc  873  dcor  902  pm5.71dc  928  dedlema  936  3mix1  1133  xoranor  1338  19.33  1443  hbor  1508  nford  1529  19.30dc  1589  19.43  1590  19.32r  1641  moor  2046  r19.32r  2553  ssun1  3207  undif3ss  3305  reuun1  3326  prmg  3612  opthpr  3667  exmidn0m  4092  issod  4209  elelsuc  4299  ordtri2or2exmidlem  4409  regexmidlem1  4416  nndceq  6361  nndcel  6362  swoord1  6424  swoord2  6425  addlocprlem  7307  msqge0  8341  mulge0  8344  ltleap  8357  nn1m1nn  8698  elnnz  9018  zletric  9052  zlelttric  9053  zmulcl  9061  zdceq  9080  zdcle  9081  zdclt  9082  ltpnf  9518  xrlttri3  9534  xrpnfdc  9576  xrmnfdc  9577  fzdcel  9771  qletric  9972  qlelttric  9973  qdceq  9975  hashfiv01gt1  10479  isum  11105  nn0o1gt2  11509  bj-trdc  12793  bj-nn0suc0  12982  triap  13058
 Copyright terms: Public domain W3C validator