Theorem olc 290

Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96.

Assertion

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

Proof of Theorem olc

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 |- (ph -> (-. ps -> ph))
2	1	orrd 250	1 |- (ph -> (ps \/ ph))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239

This theorem is referenced by:  olci 293  olcd 295  olcs 297  pm2.07 298  pm2.46 300  pm2.41 369  jaob 467  pm4.72 703  oibabs 716  pm5.75OLD 822  dedlemb 839  dedlembOLD 840  prlem2 850  dn1 855  dn1OLD 856  19.33 1443  19.33b 1444  19.33bOLD 1445  dfsb2 1595  mooran2 1824  euor2 1839  euor2OLD 1840  undif3 2854  undif4 2930  ordssun 3769  ordequn 3770  sucprcreg 5703  rankxplim3 5825  ltapr 6303  ltpnf 6717  mnflt 6718  mnfltpnf 6719  zaddcl 7374  zmulcl 7389  expeq0 7828  bcpasci 8221  infxpidmlem3 8823  0top 8905  efif1lem5 10088  usinuniop 10341  pjthlem11 10862  dfon2lem4 13852  frxp 13951  sltsgn1 14002  sltsgn2 14003  meran1 14235  facrm 14290  nxtor 14312  subtopsin2 14907  partarelt1 15273  alexsublem3 15439  isufil2 15565  prtlem90 16246  19.33-2 16335  undif3VD 16706  paddcl 17303

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