Theorem orc 867

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 863	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm1.4  869  orcd  873  orcs  875  pm2.45  881  norbi  886  pm2.67-2  891  pm2.4  906  pm1.5  919  biort  935  biorfriOLD  940  pm4.72  951  pm3.48  965  pm4.44  998  pm4.45  999  orabs  1000  pm5.61  1002  andi  1009  pm5.71  1029  dedlema  1045  consensus  1052  ifptru  1074  3mix1  1331  cad11  1617  19.33  1885  19.33b  1886  dfsb2  2495  moor  2551  ssun1  4127  reuun1  4277  opthpr  4802  prel12g  4815  opthprneg  4816  disjord  5082  elelsuc  6386  ordssun  6415  fununmo  6533  tpres  7141  fvf1pr  7247  soxp  8065  poxp2  8079  poxp3  8086  omopth2  8505  naddunif  8614  swoord1  8660  swoord2  8661  nelaneqOLD  9495  sornom  10175  fin56  10291  fpwwe2lem11  10539  ltle  11208  nn1m1nn  12153  elnnz  12485  elnn0z  12488  zmulcl  12527  nn01to3  12841  ltpnf  13021  xrltle  13050  xrltne  13064  swrdnnn0nd  14566  s3sndisj  14876  s3iunsndisj  14877  nn0o1gt2  16294  prm23lt5  16728  4sqlem17  16875  cshwsidrepswmod0  17008  cshwsdisj  17012  cshwshash  17018  funcres2c  17812  tsrlemax  18494  odlem1  19449  gexlem1  19493  drngmuleq0  20680  maducoeval2  22556  alexsubALTlem3  23965  dyadmbl  25529  gausslemma2dlem0f  27300  eln0s  28288  elnnzs  28326  nb3grprlem1  29360  frgrwopreg  30305  frgrregorufr  30307  2wspmdisj  30319  frgrregord13  30378  satfvsucsuc  35430  dfon2lem4  35849  dfrdg4  36016  btwnconn1  36166  segcon2  36170  broutsideof2  36187  lineunray  36212  meran1  36476  dissym1  36486  weiunpo  36530  bj-orim2  36621  bj-peircecurry  36623  bj-consensus  36643  bj-sbsb  36902  bj-unrab  36991  wl-orel12  37576  orfa  38142  tsor2  38208  lkrlspeqN  39290  sbor2  42325  omcl3g  43451  fzunt  43572  fzuntd  43573  fzunt1d  43574  fzuntgd  43575  ifpid1g  43611  ifpim3  43613  rp-fakeanorass  43630  or3or  44140  clsk1indlem3  44160  ntrclsk3  44187  19.33-2  44499  ax6e2ndeq  44676  uunT1  44896  undif3VD  44998  ax6e2ndeqVD  45025  ax6e2ndeqALT  45047  salexct  46456  salexct3  46464  salgencntex  46465  salgensscntex  46466  ndmafv2nrn  47346  otiunsndisjX  47403  prproropf1olem4  47630  poprelb  47648  nn0o1gt2ALTV  47818  odd2prm2  47842  clnbgrel  47952  dfclnbgr6  47980  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx13starlem2  48196  gpg5edgnedg  48254  ldepspr  48598  elfzolborelfzop1  48644  blen1b  48713  reorelicc  48835  opth1neg  48950  eximp-surprise2  49910