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 688  ecase2d 749  oplem1 770  ecase23d 919  euor2 1430  eqsn 2465  pwssun 2816  sotrieq 2852  elpwunsn 2902  ordtri3or 2969  ordeleqon 2980  ordsson 2981  ord0eln0 3013  onmindif2 3051  onsucuni2 3081  suc11 3083  limsssuc 3111  foconst 3668  pw2en 4426  pssnn 4513  preleq 4575  suc11reg 4577  rankxpsuc 4687  cardnn 4796  cardlim 4823  cardaleph 4857  iscard3 4860  nlt1pi 5005  leltnet 5494  xrleltnet 5531  nltpnftt 5539  ngtmnftt 5540  xrrebndt 5541  eqneg 5760  xrsupsslem 6023  xrinfmsslem 6024  dfn2 6059  elnnz1 6102  infxpidmlem8 7502  fctop 7592  cctop 7594  pjthlem11 9144  stadd 10083  stadd3 10085  atsseq 10182  atom1d 10188  atoml2 10218

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