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

Theorem orc 666
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 664 . . 3 (((𝜑𝜓) → (𝜑𝜓)) ↔ ((𝜑 → (𝜑𝜓)) ∧ (𝜓 → (𝜑𝜓))))
31, 2mpbi 143 . 2 ((𝜑 → (𝜑𝜓)) ∧ (𝜓 → (𝜑𝜓)))
43simpli 109 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.67-2  667  pm1.4  679  orci  683  orcd  685  orcs  687  pm2.45  690  biorfi  698  pm1.5  715  pm2.4  728  pm4.44  729  pm4.45  731  pm3.48  732  pm2.76  755  orabs  761  ordi  763  andi  765  pm4.72  770  biort  772  dcim  818  pm2.54dc  824  pm4.78i  842  pm2.85dc  845  dcor  877  pm5.71dc  903  dedlema  911  3mix1  1108  xoranor  1309  19.33  1414  hbor  1479  nford  1500  19.30dc  1559  19.43  1560  19.32r  1611  moor  2014  r19.32r  2507  ssun1  3147  undif3ss  3243  reuun1  3264  prmg  3535  opthpr  3590  issod  4109  elelsuc  4199  ordtri2or2exmidlem  4304  regexmidlem1  4311  nndceq  6190  nndcel  6191  swoord1  6249  swoord2  6250  addlocprlem  6995  msqge0  7991  mulge0  7994  ltleap  8005  nn1m1nn  8332  elnnz  8654  zletric  8688  zlelttric  8689  zmulcl  8697  zdceq  8716  zdcle  8717  zdclt  8718  ltpnf  9144  xrlttri3  9160  fzdcel  9347  qletric  9542  qlelttric  9543  qdceq  9545  hashfiv01gt1  10023  nn0o1gt2  10683  bj-nn0suc0  11186
  Copyright terms: Public domain W3C validator