Theorem orc 269

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

Syntax hints:   -> wi 3   \/ wo 222

This theorem is referenced by:  orci 270  orcd 272  orcs 274  pm2.45 277  pm2.67 282  pm2.4 344  pm4.44 345  jaob 422  pm4.43 431  pm5.61 447  pm2.74 571  pm2.75 572  pm2.8 574  orabs 579  pm4.45 638  oibabs 652  biort 732  orbidi 741  pm5.71 746  dedlema 760  consensus 765  3mix1 813  19.33 1087  19.33b 1088  dfsb2 1220  moor 1417  pssn2lp 2137  ssun1 2183  reuun1 2267  opthpr 2476  iununi 2606  pwundif 2817  elelsuc 3031  ordssun 3069  ordequn 3070  ltnet 5488  ltnetOLD 5489  ltlet 5493  ltpnft 5515  xrltlet 5532  xrltnet 5538  elnnz 6092  elnn0z 6094  zmulclt 6127  bcpasc 6907  infxpidmlem8 7502  efif1lem5 8649  iintlem1 10476

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