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  1329  norasslem2  1531  cad11  1612  19.33  1881  19.33b  1882  dfsb2  2495  moor  2551  ssun1  4187  reuun1  4333  opthpr  4855  prel12g  4868  opthprneg  4869  disjord  5136  elelsuc  6458  ordssun  6487  fununmo  6614  tpres  7220  fvf1pr  7326  soxp  8152  poxp2  8166  poxp3  8173  omopth2  8620  naddunif  8729  swoord1  8775  swoord2  8776  nelaneq  9636  sornom  10314  fin56  10430  fpwwe2lem11  10678  ltle  11346  nn1m1nn  12284  elnnz  12620  elnn0z  12623  zmulcl  12663  nn01to3  12980  ltpnf  13159  xrltle  13187  xrltne  13201  swrdnnn0nd  14690  s3sndisj  15002  s3iunsndisj  15003  nn0o1gt2  16414  prm23lt5  16847  4sqlem17  16994  cshwsidrepswmod0  17128  cshwsdisj  17132  cshwshash  17138  funcres2c  17954  tsrlemax  18643  odlem1  19567  gexlem1  19611  drngmuleq0  20779  maducoeval2  22661  alexsubALTlem3  24072  dyadmbl  25648  gausslemma2dlem0f  27419  eln0s  28372  elnnzs  28401  nb3grprlem1  29411  frgrwopreg  30351  frgrregorufr  30353  2wspmdisj  30365  frgrregord13  30424  satfvsucsuc  35349  dfon2lem4  35767  dfrdg4  35932  btwnconn1  36082  segcon2  36086  broutsideof2  36103  lineunray  36128  meran1  36393  dissym1  36403  weiunpo  36447  bj-orim2  36538  bj-peircecurry  36540  bj-consensus  36560  bj-sbsb  36819  bj-unrab  36908  wl-orel12  37491  orfa  38068  tsor2  38134  lkrlspeqN  39152  sbor2  42229  omcl3g  43323  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  ifpid1g  43483  ifpim3  43485  rp-fakeanorass  43502  or3or  44012  clsk1indlem3  44032  ntrclsk3  44059  19.33-2  44377  ax6e2ndeq  44556  uunT1  44777  undif3VD  44879  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  salexct  46289  salexct3  46297  salgencntex  46298  salgensscntex  46299  ndmafv2nrn  47171  otiunsndisjX  47228  prproropf1olem4  47430  poprelb  47448  nn0o1gt2ALTV  47618  odd2prm2  47642  clnbgrel  47752  dfclnbgr6  47779  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  ldepspr  48318  elfzolborelfzop1  48364  blen1b  48437  reorelicc  48559  eximp-surprise2  49015