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 209  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  1040  consensus  1047  ifptru  1068  3mix1  1326  norasslem2  1530  cad0  1617  cad11  1619  19.33  1884  19.33b  1885  dfsb2  2531  dfsb2ALT  2590  moor  2637  ssun1  4151  reuun1  4288  opthpr  4785  prel12g  4797  opthprneg  4798  disjord  5057  elelsuc  6266  ordssun  6293  fununmo  6404  tpres  6966  soxp  7826  omopth2  8213  swoord1  8323  swoord2  8324  nelaneq  9066  sornom  9702  fin56  9818  fpwwe2lem12  10066  ltle  10732  nn1m1nn  11661  elnnz  11994  elnn0z  11997  zmulcl  12034  nn01to3  12344  ltpnf  12518  xrltle  12545  xrltne  12559  swrdnnn0nd  14021  s3sndisj  14330  s3iunsndisj  14331  nn0o1gt2  15735  prm23lt5  16154  4sqlem17  16300  cshwsidrepswmod0  16431  cshwsdisj  16435  cshwshash  16441  funcres2c  17174  tsrlemax  17833  odlem1  18666  gexlem1  18707  drngmuleq0  19528  maducoeval2  21252  alexsubALTlem3  22660  dyadmbl  24204  gausslemma2dlem0f  25940  nb3grprlem1  27165  frgrwopreg  28105  frgrregorufr  28107  2wspmdisj  28119  frgrregord13  28178  satfvsucsuc  32616  dfon2lem4  33035  dfrdg4  33416  btwnconn1  33566  segcon2  33570  broutsideof2  33587  lineunray  33612  meran1  33763  dissym1  33773  bj-orim2  33895  bj-peircecurry  33897  bj-consensus  33915  bj-sbsb  34164  bj-unrab  34248  wl-orel12  34755  orfa  35364  tsor2  35430  lkrlspeqN  36311  sbor2  39109  ifpid1g  39866  ifpim3  39868  rp-fakeanorass  39885  or3or  40377  clsk1indlem3  40399  ntrclsk3  40426  19.33-2  40720  ax6e2ndeq  40899  uunT1  41120  undif3VD  41222  ax6e2ndeqVD  41249  ax6e2ndeqALT  41271  salexct  42624  salexct3  42632  salgencntex  42633  salgensscntex  42634  ndmafv2nrn  43428  otiunsndisjX  43485  prproropf1olem4  43675  poprelb  43693  nn0o1gt2ALTV  43866  odd2prm2  43890  ldepspr  44535  elfzolborelfzop1  44581  blen1b  44655  reorelicc  44704  eximp-surprise2  44893