Theorem orrd 240

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 231	. 2 |- ((ps \/ ch) <-> (-. ps -> ch))
3	1, 2	sylibr 207	1 |- (ph -> (ps \/ ch))

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

This theorem is referenced by:  olc 275  orc 276  pm5.63 353  sspss 2196  pwpw0 2523  sssn 2527  sspr 2529  pwsnALT 2555  pwssun 2883  ordsseleq 3033  orduniorsuc 3144  unizlim 3170  ordzsl 3173  nn0suc 3211  tfinds 3218  xpexr 3536  fvclss 3912  odi 4268  entric 4903  iscard3 4953  psslinpr 5200  lttri4 5580  ssxr 5605  xrletri 5626  letric 5685  mul0ori 5759  avgle 6105  supxrgtmnf 6174  zeo 6284  icounlem 6438  ioojoin 6442  sq01 6740  cctop 7737  clslp 7833  lmfexlem1 8041  metelcls 8050  nvmul0or 8356  hvmul0or 8977  atomli 10393  atordi 10395

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 154  df-or 231

Copyright terms: Public domain