Theorem orrd 250

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

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

This theorem is referenced by:  olc 290  orc 291  pm5.63 373  ordi 656  dn1OLD 856  sspss 2707  pwpw0 3134  sssn 3142  sspr 3144  pwsnALT 3173  unissint 3241  pwssun 3578  ordsseleqOLD 3688  ordtri2or 3766  unizlim 3786  orduniorsuc 3909  ordzsl 3927  tfindsOLD 3943  nn0suc 3976  xpexr 4352  fvclss 4831  odi 5258  entric 5990  iscard3 6036  psslinpr 6287  lttri4OLD 6685  ssxr 6714  ssxrOLD 6715  xrletri 6736  letric 6802  letricOLD 6803  mul0ori 6882  avgle 7231  supxrgtmnf 7301  zeo 7411  icounlem 7581  ioojoin 7585  sq01 7897  fctop 8920  cctop 8922  clslp 9024  lmfexlem1 9234  metelcls 9243  nvmul0or 9604  hvmul0or 10526  atomli 11954  atordi 11956  nepss 13820  dfon2lem6 13854  soseq 13955  nxtor 14312  fixpc 14418  subntr 15425  alexsublem3 15439  ufprim 15569  filssufillem 15570  uffixfr 15575  fixufil 15576  filcon 15580  uzm1 15784  fzm1 15796  pm10.57 16318

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 164  df-or 241

Copyright terms: Public domain