Theorem orc 392

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
orc	|- ( ph -> ( ph \/ ps ) )

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 112	. 2 |- ( ph -> ( -. ph -> ps ) )
2	1	orrd 385	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 375

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 190  df-or 377

This theorem is referenced by:  pm1.4  393  orcd  399  orcs  401  pm2.45  404  pm2.67-2  409  biorfi  414  pm1.5  531  pm2.4  585  pm4.44  587  pm4.45  702  pm3.48  851  orabs  873  norbi  877  andi  884  pm4.72  893  biort  913  pm5.71  950  consensus  967  dedlema  970  ifptru  994  3mix1  1199  cad0  1528  cad11  1530  19.33  1755  19.33b  1756  dfsb2  2222  moor  2375  ssun1  3588  undif3  3695  reuun1  3716  eqoreldif  4004  opthpr  4144  otsndisj  4706  otiunsndisj  4707  elelsuc  5502  ordelinel  5528  ordssun  5529  ordequn  5530  fununmo  5632  tpres  6133  soxp  6928  omopth2  7303  swoord1  7410  swoord2  7411  sornom  8725  fin56  8841  fpwwe2lem12  9084  ltle  9740  nn1m1nn  10651  elnnz  10971  elnn0z  10974  zmulcl  11009  nn01to3  11280  ltpnf  11445  xrltle  11471  xrltne  11483  4sqlem17OLD  14984  4sqlem17  14990  cshwsidrepswmod0  15143  cshwsdisj  15147  cshwshash  15153  funcres2c  15884  tsrlemax  16544  odlem1  17259  odlem1OLD  17262  gexlem1  17306  gexlem1OLD  17308  drngmuleq0  18076  maducoeval2  19742  alexsubALTlem3  21142  dyadmbl  22637  bcmono  24284  nb3graprlem1  25258  frgrawopreg  25856  frgraregorufr  25860  2spotdisj  25868  2spotiundisj  25869  2spotmdisj  25875  frgraregord13  25926  dfon2lem4  30503  sltsgn1  30619  sltsgn2  30620  dfrdg4  30789  btwnconn1  30939  segcon2  30943  broutsideof2  30960  lineunray  30985  meran1  31142  dissym1  31152  bj-consensus  31220  bj-sbsb  31505  bj-unrab  31597  wl-orel12  31919  wl-nftht  31939  orfa  32379  tsor2  32454  lkrlspeqN  32808  fnwe2lem3  35981  ifpid1g  36209  ifpim3  36211  rp-fakeanorass  36228  19.33-2  36801  ax6e2ndeq  36996  uunT1  37230  undif3VD  37342  ax6e2ndeqVD  37369  ax6e2ndeqALT  37391  disjxp1  37470  nelpr1  37499  salexct  38305  salexct3  38313  salgencntex  38314  salgensscntex  38315  nnfoctbdjlem  38409  nn0o1gt2ALTV  38968  otiunsndisjX  39152  nb3grprlem1  39618  ldepspr  40774  elfzolborelfzop1  40824  nn0o1gt2  40835  blen1b  40907  eximp-surprise2  41030