Theorem orrd 877

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 866	. 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orc  881  olc  882  pm2.68  914  pm4.79  1021  19.30  1914  axi12  2732  r19.30  3131  sspss  4053  eqoreldif  4649  pwpw0  4777  sssn  4790  unissint  4935  disjiund  5098  disjxiun  5104  otsndisj  5500  otiunsndisj  5501  pwssun  5551  isso2i  5604  ordtr3  6408  ordtri2or  6462  unizlim  6486  fvclss  7242  orduniorsuc  7830  ordzsl  7845  nn0suc  7895  xpexr  7919  soseq  8161  odi  8570  swoso  8735  erdisj  8758  ordtypelem7  9500  wemapsolem  9526  domwdom  9550  iscard3  10100  ackbij1lem18  10242  fin56  10399  entric  10569  gchdomtri  10642  inttsk  10787  r1tskina  10795  psslinpr  11044  1re  11236  ssxr  11307  letric  11338  mul0or  11882  mulge0b  12113  zeo  12711  uzm1  12925  xrletri  13208  supxrgtmnf  13385  sq01  14293  ruclem3  16327  prm2orodd  16787  phiprmpw  16873  pleval2i  18428  chnind  18715  irredn0  20570  lvecvs0or  21301  lssvs0or  21303  lspsnat  21338  lsppratlem1  21340  domnchr  21751  fctop  23235  cctop  23237  ppttop  23238  clslp  23379  restntr  23413  cnconn  23653  txindis  23866  txconn  23921  isufil2  24140  ufprim  24141  alexsubALTlem3  24281  pmltpc  25684  iundisj2  25783  limcco  26127  fta1b  26404  aalioulem2  26576  abelthlem2  26675  logreclem  27007  dchrfi  27499  2sqb  27676  nosepdmlem  27927  noetasuplem4  27980  lestric  28012  muls0ord  28458  bdayfinbndlem1  28740  tgbtwnconn1  28925  legov3  28948  coltr  29003  colline  29005  tglowdim2ln  29007  ragflat3  29068  ragperp  29079  lmieu  29176  lmicom  29180  lmimid  29186  numedglnl  29609  pthisspthorcycl  30277  nvmul0or  31139  hvmul0or  31514  atomli  32871  atordi  32873  iundisj2f  33071  iundisj2fi  33276  gsumfs2d  33509  mxidlprm  33881  ssmxidl  33885  qsdrng  33907  dflringlem3  33914  dflring4  33916  zarclssn  34391  signsply0  35067  cvmsdisj  35857  nepss  36305  dfon2lem6  36373  btwnconn1lem13  36687  wl-exeq  38305  eqvreldisj  39454  lsator0sp  39882  lkreqN  40051  2at0mat0  40406  trlator0  41052  dochkrshp4  42270  dochsat0  42338  lcfl6  42381  expeqidd  43208  sn-remul0ord  43291  rp-fakeimass  44360  frege124d  44609  clsk1independent  44894  mnringmulrcld  45074  pm10.57  45203  icccncfext  46723  fourierdlem70  47012  ichnreuop  48380  uzlidlring  49158  nneop  49464  mo0sn  49752  euendfunc2  50461