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  820  pm2.54dc  826  pm4.78i  844  pm2.85dc  847  dcor  879  pm5.71dc  905  dedlema  913  3mix1  1110  xoranor  1311  19.33  1416  hbor  1481  nford  1502  19.30dc  1561  19.43  1562  19.32r  1613  moor  2016  r19.32r  2510  ssun1  3152  undif3ss  3249  reuun1  3270  prmg  3546  opthpr  3601  issod  4122  elelsuc  4212  ordtri2or2exmidlem  4317  regexmidlem1  4324  nndceq  6216  nndcel  6217  swoord1  6275  swoord2  6276  addlocprlem  7041  msqge0  8037  mulge0  8040  ltleap  8051  nn1m1nn  8378  elnnz  8696  zletric  8730  zlelttric  8731  zmulcl  8739  zdceq  8758  zdcle  8759  zdclt  8760  ltpnf  9186  xrlttri3  9202  fzdcel  9389  qletric  9586  qlelttric  9587  qdceq  9589  hashfiv01gt1  10108  iisum  10688  nn0o1gt2  10830  bj-nn0suc0  11333
  Copyright terms: Public domain W3C validator