Theorem orc 385

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 109	. 2 |- ( ph -> ( -. ph -> ps ) )
2	1	orrd 378	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  pm1.4  386  orcd  392  orcs  394  pm2.45  397  pm2.67-2  402  biorfi  407  pm1.5  522  pm2.4  575  pm4.44  577  pm4.45  688  pm3.48  833  orabs  855  norbi  859  andi  867  pm4.72  876  biort  896  pm5.71  936  dedlema  954  consensus  959  3mix1  1165  cad1  1465  cad11  1466  cad0  1467  19.33  1696  19.33b  1697  dfsb2  2115  moor  2347  ssun1  3663  undif3  3766  reuun1  3787  opthpr  4210  otsndisj  4761  otiunsndisj  4762  elelsuc  4959  ordelinel  4985  ordssun  4986  ordequn  4987  fununmo  5637  tpres  6125  soxp  6912  omopth2  7251  swoord1  7358  swoord2  7359  sornom  8674  fin56  8790  fpwwe2lem12  9036  ltle  9690  nn1m1nn  10576  elnnz  10895  elnn0z  10898  zmulcl  10933  nn01to3  11200  ltpnf  11356  xrltle  11380  xrltne  11391  4sqlem17  14491  cshwsidrepswmod0  14591  cshwsdisj  14595  cshwshash  14601  funcres2c  15317  tsrlemax  15977  odlem1  16686  gexlem1  16726  drngmuleq0  17546  maducoeval2  19269  alexsubALTlem3  20675  dyadmbl  22135  bcmono  23678  nb3graprlem1  24578  frgrawopreg  25176  frgraregorufr  25180  2spotdisj  25188  2spotiundisj  25189  2spotmdisj  25195  frgraregord13  25246  dfon2lem4  29435  sltsgn1  29638  sltsgn2  29639  dfrdg4  29805  btwnconn1  29956  segcon2  29960  broutsideof2  29977  lineunray  30002  meran1  30081  dissym1  30091  wl-nftht  30194  orfa  30684  tsor2  30760  fnwe2lem3  31202  19.33-2  31491  otiunsndisjX  32565  ldepspr  33218  eximp-surprise2  33344  ax6e2ndeq  33475  uunT1  33720  undif3VD  33825  ax6e2ndeqVD  33852  ax6e2ndeqALT  33874  bj-consensus  34306  bj-unrab  34637  lkrlspeqN  35039  ifpid1g  37852  ifpim3  37859  rp-fakeanorass  37897