MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orc Structured version   Unicode version

Theorem orc 375
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
StepHypRef Expression
1 pm2.24 103 . 2  |-  ( ph  ->  ( -.  ph  ->  ps ) )
21orrd 368 1  |-  ( ph  ->  ( ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  pm1.4  376  orcd  382  orcs  384  pm2.45  387  pm2.67-2  392  biorfi  397  pm1.5  509  pm2.4  559  pm4.44  561  pm4.45  670  pm3.48  807  orabs  829  andi  838  pm4.72  847  biort  867  pm5.71  903  dedlema  921  consensus  926  3mix1  1126  cad1  1407  cad11  1408  cad0  1409  19.33  1617  19.33b  1618  dfsb2  2115  moor  2333  ssun1  3502  undif3  3594  reuun1  3615  opthpr  3968  elelsuc  4645  ordelinel  4672  ordssun  4673  ordequn  4674  soxp  6451  omopth2  6819  swoord1  6926  swoord2  6927  sornom  8149  fin56  8265  fpwwe2lem12  8508  ltle  9155  nn1m1nn  10012  elnnz  10284  elnn0z  10286  zmulcl  10316  ltpnf  10713  xrltle  10734  xrltne  10745  4sqlem17  13321  funcres2c  14090  tsrlemax  14644  odlem1  15165  gexlem1  15205  drngmuleq0  15850  alexsubALTlem3  18072  dyadmbl  19484  bcmono  21053  nb3graprlem1  21452  dfon2lem4  25405  sltsgn1  25608  sltsgn2  25609  dfrdg4  25787  btwnconn1  26027  segcon2  26031  broutsideof2  26048  lineunray  26073  meran1  26153  dissym1  26163  fnwe2lem3  27118  19.33-2  27548  otsndisj  28055  otiunsndisj  28056  otiunsndisjX  28057  cshwsdisj  28248  cshwssize  28253  frgrawopreg  28375  frgraregorufr  28379  2spotdisj  28387  2spotiundisj  28388  2spotmdisj  28394  a9e2ndeq  28583  uunT1  28829  undif3VD  28931  a9e2ndeqVD  28958  a9e2ndeqALT  28980  dfsb2NEW7  29575  lkrlspeqN  29906
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator