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 2135  pwpw0 2460  sssn 2464  sspr 2466  pwssun 2816  ordsseleq 2966  orduniorsuc 3077  unizlim 3103  ordzsl 3106  nn0suc 3144  tfinds 3151  xpexr 3465  fvclss 3840  odi 4194  entri 4811  iscard3 4860  psslinpr 5107  lttri4t 5487  ssxr 5513  xrletrit 5534  letrit 5594  mul0or 5663  avglet 5991  supxrgtmnf 6039  zeot 6146  icounlem 6345  sq01t 6582  fctop 7592  cctop 7594  clslp 7689  lmfexlem1 7891  metelcls 7900  nvmul0or 8212  hvmul0ort 8815  atoml 10217  atord 10219

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