Theorem ord 202

Description: Deduction from disjunction definition.

Hypothesis

Ref	Expression
ord.1	|- (ph -> (ps \/ ch))

Assertion

Ref	Expression
ord	|- (ph -> (-. ps -> ch))

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 |- (ph -> (ps \/ ch))
2		df-or 197	. 2 |- ((ps \/ ch) <-> (-. ps -> ch))
3	1, 2	sylib 173	1 |- (ph -> (-. ps -> ch))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195

This theorem is referenced by:  orcanai 515  ecase2d 558  oplem1 578  ecased 643  pwssun 1917  sotrieq 2149  ordtri3or 2230  ordeleqon 2241  ordsson 2242  ord0eln0 2278  onmindif2 2313  suc11 2341  limsssuc 2362  pw2en 3348  pssnn 3428  preleq 3454  suc11reg 3456  cardnn 3631  cardlim 3657  cardaleph 3690  iscard3 3693  nlt1pi 3827  leltnet 4287  eqneg 4378  elnnz1 4581  infxpidmlem8 4940  pjthlem11 5235  stadd 5687  stadd3 5689  atsseq 5745  atom1d 5750

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