Theorem orrd 863

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

Hypothesis

Ref	Expression
orrd.1	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
orrd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orrd

Step	Hyp	Ref	Expression
1		orrd.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2		pm2.54 852	. 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orc  867  olc  868  pm2.68  900  pm4.79  1005  19.30  1881  axi12  2699  r19.30  3100  sspss  4065  eqoreldif  4649  pwpw0  4777  sssn  4790  unissint  4936  disjiund  5098  disjxiun  5104  otsndisj  5479  otiunsndisj  5480  pwssun  5530  isso2i  5583  ordtr3  6378  ordtri2or  6432  unizlim  6457  fvclss  7215  orduniorsuc  7805  ordzsl  7821  nn0suc  7870  xpexr  7894  soseq  8138  odi  8543  swoso  8705  erdisj  8728  ordtypelem7  9477  wemapsolem  9503  domwdom  9527  iscard3  10046  ackbij1lem18  10189  fin56  10346  entric  10510  gchdomtri  10582  inttsk  10727  r1tskina  10735  psslinpr  10984  1re  11174  ssxr  11243  letric  11274  mul0or  11818  mulge0b  12053  zeo  12620  uzm1  12831  xrletri  13113  supxrgtmnf  13289  sq01  14190  ruclem3  16201  prm2orodd  16661  phiprmpw  16746  pleval2i  18295  irredn0  20332  drngmul0orOLD  20670  lvecvs0or  21018  lssvs0or  21020  lspsnat  21055  lsppratlem1  21057  domnchr  21442  fctop  22891  cctop  22893  ppttop  22894  clslp  23035  restntr  23069  cnconn  23309  txindis  23521  txconn  23576  isufil2  23795  ufprim  23796  alexsubALTlem3  23936  pmltpc  25351  iundisj2  25450  limcco  25794  fta1b  26077  aalioulem2  26241  abelthlem2  26342  logreclem  26672  dchrfi  27166  2sqb  27343  nosepdmlem  27595  noetasuplem4  27648  sletric  27676  muls0ord  28088  tgbtwnconn1  28502  legov3  28525  coltr  28574  colline  28576  tglowdim2ln  28578  ragflat3  28633  ragperp  28644  lmieu  28711  lmicom  28715  lmimid  28721  numedglnl  29071  pthisspthorcycl  29732  nvmul0or  30579  hvmul0or  30954  atomli  32311  atordi  32313  iundisj2f  32519  iundisj2fi  32720  chnind  32937  gsumfs2d  32995  mxidlprm  33441  ssmxidl  33445  qsdrng  33468  zarclssn  33863  signsply0  34542  cvmsdisj  35257  nepss  35705  dfon2lem6  35776  btwnconn1lem13  36087  wl-exeq  37522  eqvreldisj  38605  lsator0sp  38994  lkreqN  39163  2at0mat0  39519  trlator0  40165  dochkrshp4  41383  dochsat0  41451  lcfl6  41494  expeqidd  42313  sn-remul0ord  42396  rp-fakeimass  43501  frege124d  43750  clsk1independent  44035  mnringmulrcld  44217  pm10.57  44360  icccncfext  45885  fourierdlem70  46174  ichnreuop  47473  uzlidlring  48223  nneop  48515  mo0sn  48804  euendfunc2  49516