Theorem ord 232

Description: Deduce implication from disjunction.

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 224	. 2 |- ((ps \/ ch) <-> (-. ps -> ch))
3	1, 2	sylib 198	1 |- (ph -> (-. ps -> ch))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222

This theorem is referenced by:  orcanai 689  ecase2d 750  oplem1 771  ecase23d 920  euor2 1435  eqsn 2470  pwssun 2822  sotrieq 2856  elpwunsn 2907  ordtri3or 2974  ordeleqon 2985  ordsson 2986  ord0eln0 3018  onmindif2 3056  onsucuni2 3086  suc11 3088  limsssuc 3116  foconst 3674  pw2en 4432  pssnn 4519  preleq 4583  suc11reg 4585  rankxpsuc 4695  cardnn 4804  cardlim 4831  cardaleph 4865  iscard3 4868  nlt1pi 5013  leltnet 5502  xrleltnet 5539  nltpnftt 5547  ngtmnftt 5548  xrrebndt 5549  eqneg 5768  xrsupsslem 6031  xrinfmsslem 6032  dfn2 6067  elnnz1 6110  infxpidmlem8 7510  fctop 7600  cctop 7602  pjthlem11 9167  stadd 10111  stadd3 10113  atsseq 10211  atom1d 10217  atoml2 10247

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