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  2731  r19.30  3130  sspss  4050  eqoreldif  4646  pwpw0  4774  sssn  4787  unissint  4932  disjiund  5094  disjxiun  5100  otsndisj  5492  otiunsndisj  5493  pwssun  5543  isso2i  5596  ordtr3  6410  ordtri2or  6464  unizlim  6488  fvclss  7246  orduniorsuc  7842  ordzsl  7857  nn0suc  7907  xpexr  7931  soseq  8177  odi  8588  swoso  8753  erdisj  8776  ordtypelem7  9519  wemapsolem  9545  domwdom  9569  iscard3  10173  ackbij1lem18  10315  fin56  10472  entric  10642  gchdomtri  10715  inttsk  10860  r1tskina  10868  psslinpr  11117  1re  11309  ssxr  11380  letric  11411  mul0or  11957  mulge0b  12188  zeo  12786  uzm1  13000  xrletri  13283  supxrgtmnf  13460  sq01  14370  ruclem3  16402  prm2orodd  16867  phiprmpw  16954  pleval2i  18509  chnind  18796  irredn0  20654  lvecvs0or  21387  lssvs0or  21389  lspsnat  21424  lsppratlem1  21426  domnchr  21839  fctop  23323  cctop  23325  ppttop  23326  clslp  23467  restntr  23501  cnconn  23741  txindis  23954  txconn  24009  isufil2  24228  ufprim  24229  alexsubALTlem3  24369  pmltpc  25772  iundisj2  25871  limcco  26214  fta1b  26491  aalioulem2  26661  abelthlem2  26760  logreclem  27091  dchrfi  27583  2sqb  27760  nosepdmlem  28041  noetasuplem4  28094  lestric  28126  muls0ord  28572  bdayfinbndlem1  28854  tgbtwnconn1  29039  legov3  29062  coltr  29117  colline  29119  tglowdim2ln  29121  ragflat3  29182  ragperp  29193  lmieu  29290  lmicom  29294  lmimid  29300  numedglnl  29723  pthisspthorcycl  30391  nvmul0or  31253  hvmul0or  31628  atomli  32985  atordi  32987  iundisj2f  33185  iundisj2fi  33390  gsumfs2d  33623  mxidlprm  33996  ssmxidl  34000  qsdrng  34022  dflringlem3  34029  dflring4  34031  zarclssn  34506  signsply0  35181  cvmsdisj  36036  nepss  36484  dfon2lem6  36551  btwnconn1lem13  36865  wl-exeq  38468  eqvreldisj  39632  lsator0sp  40060  lkreqN  40229  2at0mat0  40584  trlator0  41230  dochkrshp4  42448  dochsat0  42516  lcfl6  42559  expeqidd  43384  sn-remul0ord  43461  rp-fakeimass  44514  frege124d  44762  clsk1independent  45047  mnringmulrcld  45227  pm10.57  45356  icccncfext  46898  fourierdlem70  47187  ichnreuop  48555  uzlidlring  49333  nneop  49639  mo0sn  49927  euendfunc2  50636