Theorem orc 862

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
orc	⊢ (𝜑 → (𝜑 ∨ 𝜓))

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 124	. 2 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))
2	1	orrd 858	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-or 843

This theorem is referenced by:  pm1.4  864  orcd  870  orcs  872  pm2.45  876  norbi  881  pm2.67-2  886  pm2.4  901  pm1.5  914  biort  930  biorfi  933  pm4.72  944  pm3.48  958  pm4.44  991  pm4.45  992  orabs  993  pm5.61  995  andi  1002  pm5.71  1022  dedlema  1038  consensus  1045  ifptru  1066  3mix1  1323  cad0  1599  cad11  1601  19.33  1866  19.33b  1867  dfsb2  2486  dfsb2ALT  2545  moor  2594  ssun1  4069  reuun1  4205  opthpr  4689  prel12g  4701  opthprneg  4702  disjord  4951  elelsuc  6138  ordssun  6165  fununmo  6271  tpres  6830  soxp  7676  omopth2  8060  swoord1  8170  swoord2  8171  nelaneq  8909  sornom  9545  fin56  9661  fpwwe2lem12  9909  ltle  10576  nn1m1nn  11506  elnnz  11839  elnn0z  11842  zmulcl  11880  nn01to3  12190  ltpnf  12365  xrltle  12392  xrltne  12406  swrdnnn0nd  13854  s3sndisj  14161  s3iunsndisj  14162  nn0o1gt2  15565  prm23lt5  15980  4sqlem17  16126  cshwsidrepswmod0  16257  cshwsdisj  16261  cshwshash  16267  funcres2c  17000  tsrlemax  17659  odlem1  18394  gexlem1  18434  drngmuleq0  19215  maducoeval2  20933  alexsubALTlem3  22341  dyadmbl  23884  gausslemma2dlem0f  25619  nb3grprlem1  26845  frgrwopreg  27794  frgrregorufr  27796  2wspmdisj  27808  frgrregord13  27867  satfvsucsuc  32220  dfon2lem4  32639  dfrdg4  33021  btwnconn1  33171  segcon2  33175  broutsideof2  33192  lineunray  33217  meran1  33368  dissym1  33378  bj-orim2  33497  bj-peircecurry  33499  bj-consensus  33517  bj-sbsb  33730  bj-unrab  33815  wl-orel12  34282  orfa  34892  tsor2  34958  lkrlspeqN  35838  sbor2  38633  ifpid1g  39345  ifpim3  39347  rp-fakeanorass  39364  or3or  39856  clsk1indlem3  39878  ntrclsk3  39905  19.33-2  40252  ax6e2ndeq  40432  uunT1  40653  undif3VD  40755  ax6e2ndeqVD  40782  ax6e2ndeqALT  40804  salexct  42159  salexct3  42167  salgencntex  42168  salgensscntex  42169  ndmafv2nrn  42937  otiunsndisjX  42994  prproropf1olem4  43150  poprelb  43168  nn0o1gt2ALTV  43341  odd2prm2  43365  ldepspr  44008  elfzolborelfzop1  44055  blen1b  44129  reorelicc  44178  eximp-surprise2  44366