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 690  ecase2d 751  oplem1 772  ecase23d 922  euor2 1437  eqsn 2474  pwssun 2827  sotrieq 2861  elpwunsn 2912  ordtri3or 2979  ordeleqon 2990  ordsson 2991  ord0eln0 3023  onmindif2 3061  onsucuni2 3091  suc11 3093  limsssuc 3121  foconst 3683  pw2en 4446  pssnn 4534  preleq 4603  suc11reg 4605  rankxpsuc 4715  cardnn 4824  cardlim 4851  cardaleph 4885  iscard3 4888  nlt1pi 5033  leltnet 5521  xrleltnet 5558  nltpnftt 5566  ngtmnftt 5567  xrrebndt 5568  eqneg 5804  xrsupsslem 6076  xrinfmsslem 6077  dfn2 6112  elnnz1 6155  infxpidmlem8 7559  fctopOLD 7650  cctop 7652  pjthlem11 9229  stadd 10173  stadd3 10175  atsseq 10274  atom1d 10280  atoml2 10310

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