Theorem olc 224

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

Assertion

Ref	Expression
olc	⊢ (φ → (ψ ∨ φ))

Proof of Theorem olc

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 ⊢ (φ → (¬ ψ → φ))
2	1	orrd 203	1 ⊢ (φ → (ψ ∨ φ))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195

This theorem is referenced by:  olci 227  pm2.46 229  jaob 328  pm4.72 485  oibabs 493  dedlemb 570  19.33 770  19.33b 771  ordssun 2330  ordequn 2331  sucprcreg 3451  ltapr 3945  sqge0 4344  0nn0 4546  nnnegz 4566  zaddclt 4590  zmulclt 4596  infxpidmlem3 4935  pjthlem11 5235

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

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org