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 422  pm4.72 639  oibabs 652  pm5.75 747  dedlemb 761  19.33 1087  19.33b 1088  dfsb2 1220  euor2 1430  ordssun 3069  ordequn 3070  sucprcreg 4572  rankxplim3 4686  ltapr 5123  ltpnft 5515  mnfltt 5516  mnfltpnf 5517  zaddclt 6112  zmulclt 6127  expeq0t 6517  bcpasc 6907  infxpidmlem3 7497  0top 7577  efif1lem5 8649  pjthlem11 9144

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