Theorem orc 225

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104.

Assertion

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

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 72	. 2 ⊢ (φ → (¬ φ → ψ))
2	1	orrd 203	1 ⊢ (φ → (φ ∨ ψ))

Syntax hints:   → wi 2   ∨ wo 195

This theorem is referenced by:  orci 226  pm2.45 228  pm2.67 231  jaob 328  oel 441  oibabs 493  orbidi 510  biort 550  dedlema 569  consensus 574  3mix1 600  19.33 770  19.33b 771  moor 1048  sbc2or 1454  pssn2lp 1571  ssun1 1621  pri1 1841  iununi 2037  so 2152  elelsuc 2295  ordssun 2330  ordequn 2331  ltnet 4282  ltlet 4286  elnnz 4572  0z 4573  elnn0z 4574  zaddclt 4590  zmulclt 4596  sqrge0 4760  infxpidmlem8 4940

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