Theorem orc 291

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104.

Assertion

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

Proof of Theorem orc

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

Syntax hints:   -> wi 3   \/ wo 239

This theorem is referenced by:  orci 292  orcd 294  orcs 296  pm2.45 299  pm2.67 304  pm2.4 371  pm4.44 372  jaob 467  pm4.43 477  pm5.61 496  pm2.74OLD 633  pm2.75 634  pm2.8 636  orabs 641  pm4.45 702  oibabs 716  biort 806  orbidi 815  pm5.71 820  dedlema 837  dedlemaOLD 838  consensus 844  consensusOLD 845  prlem2 850  dn1 855  3mix1 1045  19.33 1443  19.33b 1444  19.33bOLD 1445  dfsb2 1595  moor 1821  pssn2lpOLD 2710  ssun1 2767  undif3 2854  reuun1 2872  opthpr 3156  iununi 3331  iununiOLD 3332  pwundif 3579  elelsuc 3737  trsuc2 3754  ordssun 3769  ordequn 3770  ltne 6686  ltle 6690  ltpnf 6717  xrltle 6734  xrltne 6740  elnnz 7354  elnn0z 7356  zmulcl 7389  bcpasci 8221  infxpidmlem8 8828  efif1lem5 10088  trsuc2OLD 13793  dfon2lem4 13852  soxp 13950  sltsgn1 14002  sltsgn2 14003  meran1 14235  dissym1 14245  trcrm 14286  anymptr 14289  nxtor 14312  evpexun 14322  subtopsin2 14907  iintlem1 15010  partarelt1 15273  alexsublem3 15439  t1t0 15547  isufil2 15565  fsumlt1 15831  19.33-2 16335  undif3VD 16706

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241

Copyright terms: Public domain