Theorem orrd 378

Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)

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		pm2.54 374	. 2 |- ( ( -. ps -> ch ) -> ( ps \/ ch ) )
3	1, 2	syl 16	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370

This theorem is referenced by:  olc  384  orc  385  pm2.68  410  pm4.79  578  axi12  2412  axbnd  2413  sspss  3443  pwpw0  4009  sssn  4019  pwsnALT  4074  unissint  4140  disjxiun  4277  pwssun  4614  ordtr3  4751  ordtri2or  4801  unizlim  4822  fvclss  5946  orduniorsuc  6430  ordzsl  6445  nn0suc  6489  xpexr  6507  odi  7006  swoso  7120  erdisj  7136  ordtypelem7  7726  wemapsolem  7752  domwdom  7777  iscard3  8251  ackbij1lem18  8394  fin56  8550  entric  8709  gchdomtri  8784  inttsk  8929  r1tskina  8937  psslinpr  9188  ssxr  9432  letric  9463  mul0or  9964  mulge0b  10187  zeo  10715  uzm1  10879  xrletri  11116  supxrgtmnf  11280  fzm1  11524  sq01  11970  ruclem3  13498  phiprmpw  13834  pleval2i  15117  irredn0  16729  drngmul0or  16777  lvecvs0or  17111  lssvs0or  17113  lspsnat  17148  lsppratlem1  17150  domnchr  17805  fctop  18450  cctop  18452  ppttop  18453  clslp  18594  restntr  18628  cnconn  18868  txindis  19049  txcon  19104  isufil2  19323  ufprim  19324  alexsubALTlem3  19463  pmltpc  20776  iundisj2  20872  limcco  21210  fta1b  21526  aalioulem2  21684  abelthlem2  21782  logreclem  22099  dchrfi  22479  2sqb  22602  tgbtwnconn1  22883  colline  22918  nvmul0or  23855  hvmul0or  24250  atomli  25609  atordi  25611  iundisj2f  25756  iundisj2fi  25904  signsply0  26800  cvmsdisj  27007  nepss  27221  dfon2lem6  27448  soseq  27562  btwnconn1lem13  27977  wl-exeq  28211  pm10.57  29468  lsator0sp  32219  lkreqN  32388  2at0mat0  32742  trlator0  33388  dochkrshp4  34607  dochsat0  34675  lcfl6  34718