Theorem orc 878

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  pm1.4  880  orcd  884  orcs  886  pm2.45  892  norbi  897  pm2.67-2  902  pm2.4  917  pm1.5  930  biort  946  biorfriOLD  951  pm4.72  962  pm3.48  976  pm4.44  1009  pm4.45  1010  orabs  1011  pm5.61  1013  andi  1020  pm5.71  1040  dedlema  1056  consensus  1063  ifptru  1085  3mix1  1343  cad11  1635  19.33  1903  19.33b  1904  dfsb2  2523  moor  2580  ssun1  4130  reuun1  4280  opthpr  4808  prel12g  4821  opthprneg  4822  disjord  5088  el  5404  elelsuc  6417  ordssun  6446  fununmo  6564  tpres  7181  fvf1pr  7287  soxp  8104  poxp2  8118  poxp3  8125  omopth2  8548  naddunif  8659  swoord1  8706  swoord2  8707  nelaneqOLDOLD  9549  sornom  10231  fin56  10347  fpwwe2lem11  10596  ltle  11268  nn1m1nn  12228  elnnz  12575  elnn0z  12578  zmulcl  12617  nn01to3  12939  ltpnf  13119  xrltle  13148  xrltne  13162  swrdnnn0nd  14667  s3sndisj  14977  s3iunsndisj  14978  nn0o1gt2  16398  prm23lt5  16833  4sqlem17  16980  cshwsidrepswmod0  17113  cshwsdisj  17117  cshwshash  17123  funcres2c  17919  tsrlemax  18601  odlem1  19558  gexlem1  19602  drngmuleq0  20792  maducoeval2  22680  alexsubALTlem3  24089  dyadmbl  25642  gausslemma2dlem0f  27402  eln0s  28431  elnnzs  28471  bdayfinbndlem2  28538  nb3grprlem1  29527  frgrwopreg  30471  frgrregorufr  30473  2wspmdisj  30485  frgrregord13  30544  satfvsucsuc  35679  dfon2lem4  36098  dfrdg4  36265  btwnconn1  36415  segcon2  36419  broutsideof2  36436  lineunray  36461  meran1  36735  dissym1  36745  weiunpo  36789  axtco1from2  36799  bj-orim2  36962  bj-peircecurry  36964  bj-consensus  36985  bj-sbsb  37286  bj-unrab  37375  bj-axseprep  37523  wl-orel12  37978  orfa  38545  tsor2  38611  lkrlspeqN  39759  sbor2  42793  omcl3g  43875  fzunt  43995  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  ifpid1g  44034  ifpim3  44036  rp-fakeanorass  44053  or3or  44563  clsk1indlem3  44583  ntrclsk3  44610  19.33-2  44922  ax6e2ndeq  45099  uunT1  45319  undif3VD  45421  ax6e2ndeqVD  45448  ax6e2ndeqALT  45470  salexct  46872  salexct3  46880  salgencntex  46881  salgensscntex  46882  ndmafv2nrn  47780  otiunsndisjX  47837  prproropf1olem4  48076  poprelb  48094  nn0o1gt2ALTV  48280  odd2prm2  48304  clnbgrel  48414  dfclnbgr6  48442  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx13starlem2  48658  gpg5edgnedg  48716  ldepspr  49059  elfzolborelfzop1  49105  blen1b  49174  reorelicc  49296  opth1neg  49411  eximp-surprise2  50370