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 2141  pwpw0 2465  sssn 2469  sspr 2471  pwssun 2822  ordsseleq 2971  orduniorsuc 3082  unizlim 3108  ordzsl 3111  nn0suc 3149  tfinds 3156  xpexr 3471  fvclss 3846  odi 4200  entri 4819  iscard3 4868  psslinpr 5115  lttri4t 5495  ssxr 5521  xrletrit 5542  letrit 5602  mul0or 5671  avglet 5999  supxrgtmnf 6047  zeot 6154  icounlem 6353  sq01t 6590  fctop 7600  cctop 7602  clslp 7698  lmfexlem1 7907  metelcls 7916  nvmul0or 8224  hvmul0ort 8833  atoml 10246  atord 10248

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