Theorem orc 863

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  pm1.4  865  orcd  869  orcs  871  pm2.45  878  norbi  883  pm2.67-2  888  pm2.4  903  pm1.5  916  biort  932  biorfi  935  pm4.72  946  pm3.48  960  pm4.44  993  pm4.45  994  orabs  995  pm5.61  997  andi  1004  pm5.71  1024  dedlema  1042  consensus  1049  ifptru  1072  3mix1  1328  norasslem2  1533  cad11  1619  cad0OLD  1622  19.33  1888  19.33b  1889  dfsb2  2497  moor  2554  ssun1  4102  reuun1  4248  opthpr  4779  prel12g  4791  opthprneg  4792  disjord  5058  elelsuc  6323  ordssun  6350  fununmo  6465  tpres  7058  soxp  7941  omopth2  8377  swoord1  8487  swoord2  8488  nelaneq  9288  sornom  9964  fin56  10080  fpwwe2lem11  10328  ltle  10994  nn1m1nn  11924  elnnz  12259  elnn0z  12262  zmulcl  12299  nn01to3  12610  ltpnf  12785  xrltle  12812  xrltne  12826  swrdnnn0nd  14297  s3sndisj  14606  s3iunsndisj  14607  nn0o1gt2  16018  prm23lt5  16443  4sqlem17  16590  cshwsidrepswmod0  16724  cshwsdisj  16728  cshwshash  16734  funcres2c  17533  tsrlemax  18219  odlem1  19058  gexlem1  19099  drngmuleq0  19929  maducoeval2  21697  alexsubALTlem3  23108  dyadmbl  24669  gausslemma2dlem0f  26414  nb3grprlem1  27650  frgrwopreg  28588  frgrregorufr  28590  2wspmdisj  28602  frgrregord13  28661  satfvsucsuc  33227  dfon2lem4  33668  poxp2  33717  poxp3  33723  dfrdg4  34180  btwnconn1  34330  segcon2  34334  broutsideof2  34351  lineunray  34376  meran1  34527  dissym1  34537  bj-orim2  34663  bj-peircecurry  34665  bj-consensus  34686  bj-sbsb  34947  bj-unrab  35041  wl-orel12  35597  orfa  36167  tsor2  36233  lkrlspeqN  37112  sbor2  40105  ifpid1g  40999  ifpim3  41001  rp-fakeanorass  41018  or3or  41520  clsk1indlem3  41542  ntrclsk3  41569  19.33-2  41889  ax6e2ndeq  42068  uunT1  42289  undif3VD  42391  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  salexct  43763  salexct3  43771  salgencntex  43772  salgensscntex  43773  ndmafv2nrn  44601  otiunsndisjX  44658  prproropf1olem4  44846  poprelb  44864  nn0o1gt2ALTV  45034  odd2prm2  45058  ldepspr  45702  elfzolborelfzop1  45748  blen1b  45822  reorelicc  45944  eximp-surprise2  46375