Theorem orrd 233

Description: Deduce implication from disjunction.

Hypothesis

Ref	Expression
orrd.1	|- (ph -> (-. ps -> ch))

Assertion

Ref	Expression
orrd	|- (ph -> (ps \/ ch))

Proof of Theorem orrd

Step	Hyp	Ref	Expression
1		orrd.1	. 2 |- (ph -> (-. ps -> ch))
2		df-or 224	. 2 |- ((ps \/ ch) <-> (-. ps -> ch))
3	1, 2	sylibr 200	1 |- (ph -> (ps \/ ch))

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

This theorem is referenced by:  olc 268  orc 269  pm5.63 346  sspss 2145  pwpw0 2469  sssn 2473  sspr 2475  pwsnALT 2501  pwssun 2827  ordsseleq 2976  orduniorsuc 3087  unizlim 3113  ordzsl 3116  nn0suc 3154  tfinds 3161  xpexr 3479  fvclss 3855  odi 4210  entri 4839  iscard3 4888  psslinpr 5135  lttri4t 5515  ssxr 5540  xrletrit 5561  letrit 5620  mul0or 5694  avglet 6044  supxrgtmnf 6092  zeot 6199  icounlem 6412  ioojoint 6416  sq01t 6651  fctopOLD 7650  cctop 7652  clslp 7748  lmfexlem1 7956  metelcls 7965  nvmul0or 8272  hvmul0ort 8894  atoml 10309  atord 10311

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