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  6431  ordssun  6460  fununmo  6579  tpres  7199  fvf1pr  7307  soxp  8130  poxp2  8144  poxp3  8151  omopth2  8576  naddunif  8687  swoord1  8734  swoord2  8735  nelaneqOLDOLD  9582  sornom  10336  fin56  10452  fpwwe2lem11  10707  ltle  11379  nn1m1nn  12337  elnnz  12684  elnn0z  12687  zmulcl  12726  nn01to3  13049  ltpnf  13230  xrltle  13259  xrltne  13273  swrdnnn0nd  14786  s3sndisj  15100  s3iunsndisj  15101  nn0o1gt2  16531  prm23lt5  16972  4sqlem17  17119  cshwsidrepswmod0  17252  cshwsdisj  17256  cshwshash  17262  funcres2c  18058  tsrlemax  18740  odlem1  19729  gexlem1  19773  drngmuleq0  21000  maducoeval2  22935  alexsubALTlem3  24348  dyadmbl  25901  gausslemma2dlem0f  27670  eln0s  28729  elnnzs  28769  bdayfinbndlem2  28836  nb3grprlem1  29943  frgrwopreg  30906  frgrregorufr  30908  2wspmdisj  30920  frgrregord13  30979  satfvsucsuc  36099  dfon2lem4  36518  dfrdg4  36685  btwnconn1  36836  segcon2  36840  broutsideof2  36857  lineunray  36882  meran1  37169  dissym1  37179  weiunpo  37223  axtco1from2  37233  bj-orim2  37395  bj-peircecurry  37397  bj-consensus  37418  bj-sbsb  37719  bj-unrab  37809  bj-axseprep  37958  wl-orel12  38411  negprop  38611  impprop  38612  orfa  38984  tsor2  39048  lkrlspeqN  40196  sbor2  43232  omcl3g  44294  fzunt  44414  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  ifpid1g  44453  ifpim3  44455  rp-fakeanorass  44472  or3or  44982  clsk1indlem3  45002  ntrclsk3  45029  19.33-2  45325  ax6e2ndeq  45501  uunT1  45721  undif3VD  45823  ax6e2ndeqVD  45850  ax6e2ndeqALT  45872  salexct  47288  salexct3  47296  salgencntex  47297  salgensscntex  47298  ndmafv2nrn  48236  otiunsndisjX  48293  prproropf1olem4  48532  poprelb  48550  nn0o1gt2ALTV  48736  odd2prm2  48760  clnbgrel  48870  dfclnbgr6  48898  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx13starlem2  49114  gpg5edgnedg  49172  ldepspr  49529  elfzolborelfzop1  49575  blen1b  49644  reorelicc  49766  opth1neg  49880  eximp-surprise2  50825