Theorem orc 881

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 125	. 2 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))
2	1	orrd 877	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm1.4  883  orcd  887  orcs  889  pm2.45  895  norbi  900  pm2.67-2  905  pm2.4  920  pm1.5  933  biort  949  pm4.72  964  pm3.48  978  pm4.44  1012  pm4.45  1013  orabs  1014  pm5.61  1016  andi  1025  pm5.71  1045  dedlema  1061  consensus  1068  ifptru  1091  3mix1  1349  cad11  1649  19.33  1917  19.33b  1918  dfsb2  2523  moor  2580  ssun1  4124  reuun1  4274  opthpr  4811  prel12g  4824  opthprneg  4825  disjord  5092  el  5406  elelsuc  6438  ordssun  6467  fununmo  6587  tpres  7207  fvf1pr  7315  soxp  8141  poxp2  8160  poxp3  8167  omopth2  8592  naddunif  8703  swoord1  8750  swoord2  8751  nelaneqOLDOLD  9598  sornom  10355  fin56  10471  fpwwe2lem11  10726  ltle  11398  nn1m1nn  12356  elnnz  12703  elnn0z  12706  zmulcl  12745  nn01to3  13068  ltpnf  13249  xrltle  13278  xrltne  13292  swrdnnn0nd  14806  s3sndisj  15120  s3iunsndisj  15121  nn0o1gt2  16551  prm23lt5  16992  4sqlem17  17139  cshwsidrepswmod0  17272  cshwsdisj  17276  cshwshash  17282  funcres2c  18078  tsrlemax  18760  odlem1  19749  gexlem1  19793  drngmuleq0  21020  maducoeval2  22955  alexsubALTlem3  24368  dyadmbl  25921  gausslemma2dlem0f  27688  eln0s  28747  elnnzs  28787  bdayfinbndlem2  28854  nb3grprlem1  29961  frgrwopreg  30924  frgrregorufr  30926  2wspmdisj  30938  frgrregord13  30997  satfvsucsuc  36130  dfon2lem4  36548  dfrdg4  36715  btwnconn1  36866  segcon2  36870  broutsideof2  36887  lineunray  36912  meran1  37199  dissym1  37209  weiunpo  37253  axtco1from2  37263  bj-orim2  37425  bj-peircecurry  37427  bj-consensus  37448  bj-sbsb  37749  bj-unrab  37839  bj-axseprep  37990  wl-orel12  38443  negprop  38643  impprop  38644  orfa  39016  tsor2  39080  lkrlspeqN  40228  sbor2  43264  omcl3g  44335  fzunt  44455  fzuntd  44456  fzunt1d  44457  fzuntgd  44458  ifpid1g  44494  ifpim3  44496  rp-fakeanorass  44513  or3or  45022  clsk1indlem3  45042  ntrclsk3  45069  19.33-2  45365  ax6e2ndeq  45541  uunT1  45761  undif3VD  45863  ax6e2ndeqVD  45890  ax6e2ndeqALT  45912  salexct  47343  salexct3  47351  salgencntex  47352  salgensscntex  47353  ndmafv2nrn  48291  otiunsndisjX  48348  prproropf1olem4  48587  poprelb  48605  nn0o1gt2ALTV  48791  odd2prm2  48815  clnbgrel  48925  dfclnbgr6  48953  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  gpg5edgnedg  49227  ldepspr  49584  elfzolborelfzop1  49630  blen1b  49699  reorelicc  49821  opth1neg  49935  eximp-surprise2  50880