Theorem orc 866

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  pm1.4  868  orcd  872  orcs  874  pm2.45  881  norbi  886  pm2.67-2  891  pm2.4  906  pm1.5  919  biort  935  biorfi  938  pm4.72  949  pm3.48  963  pm4.44  996  pm4.45  997  orabs  998  pm5.61  1000  andi  1007  pm5.71  1027  dedlema  1045  consensus  1052  ifptru  1075  3mix1  1331  norasslem2  1537  cad11  1618  cad0OLD  1621  19.33  1888  19.33b  1889  dfsb2  2493  moor  2549  ssun1  4171  reuun1  4316  opthpr  4851  prel12g  4863  opthprneg  4864  disjord  5135  elelsuc  6434  ordssun  6463  fununmo  6592  tpres  7197  soxp  8110  poxp2  8124  poxp3  8131  omopth2  8580  naddunif  8688  swoord1  8730  swoord2  8731  nelaneq  9590  sornom  10268  fin56  10384  fpwwe2lem11  10632  ltle  11298  nn1m1nn  12229  elnnz  12564  elnn0z  12567  zmulcl  12607  nn01to3  12921  ltpnf  13096  xrltle  13124  xrltne  13138  swrdnnn0nd  14602  s3sndisj  14910  s3iunsndisj  14911  nn0o1gt2  16320  prm23lt5  16743  4sqlem17  16890  cshwsidrepswmod0  17024  cshwsdisj  17028  cshwshash  17034  funcres2c  17848  tsrlemax  18535  odlem1  19396  gexlem1  19440  drngmuleq0  20334  maducoeval2  22124  alexsubALTlem3  23535  dyadmbl  25099  gausslemma2dlem0f  26844  nb3grprlem1  28617  frgrwopreg  29556  frgrregorufr  29558  2wspmdisj  29570  frgrregord13  29629  satfvsucsuc  34294  dfon2lem4  34696  dfrdg4  34861  btwnconn1  35011  segcon2  35015  broutsideof2  35032  lineunray  35057  meran1  35234  dissym1  35244  bj-orim2  35370  bj-peircecurry  35372  bj-consensus  35393  bj-sbsb  35653  bj-unrab  35744  wl-orel12  36318  orfa  36888  tsor2  36954  lkrlspeqN  37979  sbor2  40975  omcl3g  42017  fzunt  42139  fzuntd  42140  fzunt1d  42141  fzuntgd  42142  ifpid1g  42178  ifpim3  42180  rp-fakeanorass  42197  or3or  42707  clsk1indlem3  42727  ntrclsk3  42754  19.33-2  43074  ax6e2ndeq  43253  uunT1  43474  undif3VD  43576  ax6e2ndeqVD  43603  ax6e2ndeqALT  43625  salexct  44985  salexct3  44993  salgencntex  44994  salgensscntex  44995  ndmafv2nrn  45865  otiunsndisjX  45922  prproropf1olem4  46109  poprelb  46127  nn0o1gt2ALTV  46297  odd2prm2  46321  ldepspr  47056  elfzolborelfzop1  47102  blen1b  47176  reorelicc  47298  eximp-surprise2  47734