Theorem olc 268

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 233	1 |- (ph -> (ps \/ ph))

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

This theorem is referenced by:  olci 271  olcd 273  olcs 275  pm2.07 276  pm2.46 278  pm2.41 342  jaob 424  pm4.72 643  oibabs 656  pm5.75 751  dedlemb 765  19.33 1093  19.33b 1094  dfsb2 1227  euor2 1440  ordssun 3085  ordequn 3086  sucprcreg 4609  rankxplim3 4724  ltapr 5163  ltpnft 5554  mnfltt 5555  mnfltpnf 5556  zaddclt 6167  zmulclt 6182  expeq0t 6586  bcpasc 6969  infxpidmlem3 7555  0top 7634  efif1lem5 8729  pjthlem11 9224

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 147  df-or 224

Copyright terms: Public domain