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  1616  19.33  1884  19.33b  1885  dfsb2  2492  moor  2548  ssun1  4144  reuun1  4294  opthpr  4818  prel12g  4831  opthprneg  4832  disjord  5099  elelsuc  6410  ordssun  6439  fununmo  6566  tpres  7178  fvf1pr  7285  soxp  8111  poxp2  8125  poxp3  8132  omopth2  8551  naddunif  8660  swoord1  8706  swoord2  8707  nelaneq  9559  sornom  10237  fin56  10353  fpwwe2lem11  10601  ltle  11269  nn1m1nn  12214  elnnz  12546  elnn0z  12549  zmulcl  12589  nn01to3  12907  ltpnf  13087  xrltle  13116  xrltne  13130  swrdnnn0nd  14628  s3sndisj  14940  s3iunsndisj  14941  nn0o1gt2  16358  prm23lt5  16792  4sqlem17  16939  cshwsidrepswmod0  17072  cshwsdisj  17076  cshwshash  17082  funcres2c  17872  tsrlemax  18552  odlem1  19472  gexlem1  19516  drngmuleq0  20679  maducoeval2  22534  alexsubALTlem3  23943  dyadmbl  25508  gausslemma2dlem0f  27279  eln0s  28258  elnnzs  28296  nb3grprlem1  29314  frgrwopreg  30259  frgrregorufr  30261  2wspmdisj  30273  frgrregord13  30332  satfvsucsuc  35359  dfon2lem4  35781  dfrdg4  35946  btwnconn1  36096  segcon2  36100  broutsideof2  36117  lineunray  36142  meran1  36406  dissym1  36416  weiunpo  36460  bj-orim2  36551  bj-peircecurry  36553  bj-consensus  36573  bj-sbsb  36832  bj-unrab  36921  wl-orel12  37506  orfa  38083  tsor2  38149  lkrlspeqN  39171  sbor2  42207  omcl3g  43330  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  ifpid1g  43490  ifpim3  43492  rp-fakeanorass  43509  or3or  44019  clsk1indlem3  44039  ntrclsk3  44066  19.33-2  44378  ax6e2ndeq  44556  uunT1  44776  undif3VD  44878  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  salexct  46339  salexct3  46347  salgencntex  46348  salgensscntex  46349  ndmafv2nrn  47227  otiunsndisjX  47284  prproropf1olem4  47511  poprelb  47529  nn0o1gt2ALTV  47699  odd2prm2  47723  clnbgrel  47833  dfclnbgr6  47860  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067  ldepspr  48466  elfzolborelfzop1  48512  blen1b  48581  reorelicc  48703  opth1neg  48818  eximp-surprise2  49778