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  2705  r19.30  3107  sspss  4077  eqoreldif  4661  pwpw0  4789  sssn  4802  unissint  4948  disjiund  5110  disjxiun  5116  otsndisj  5494  otiunsndisj  5495  pwssun  5545  isso2i  5598  ordtr3  6398  ordtri2or  6451  unizlim  6476  fvclss  7232  orduniorsuc  7822  ordzsl  7838  nn0suc  7888  xpexr  7912  soseq  8156  odi  8589  swoso  8751  erdisj  8771  ordtypelem7  9536  wemapsolem  9562  domwdom  9586  iscard3  10105  ackbij1lem18  10248  fin56  10405  entric  10569  gchdomtri  10641  inttsk  10786  r1tskina  10794  psslinpr  11043  ssxr  11302  letric  11333  mul0or  11875  mulge0b  12110  zeo  12677  uzm1  12888  xrletri  13167  supxrgtmnf  13343  sq01  14241  ruclem3  16249  prm2orodd  16708  phiprmpw  16793  pleval2i  18344  irredn0  20381  drngmul0orOLD  20719  lvecvs0or  21067  lssvs0or  21069  lspsnat  21104  lsppratlem1  21106  domnchr  21491  fctop  22940  cctop  22942  ppttop  22943  clslp  23084  restntr  23118  cnconn  23358  txindis  23570  txconn  23625  isufil2  23844  ufprim  23845  alexsubALTlem3  23985  pmltpc  25401  iundisj2  25500  limcco  25844  fta1b  26127  aalioulem2  26291  abelthlem2  26392  logreclem  26722  dchrfi  27216  2sqb  27393  nosepdmlem  27645  noetasuplem4  27698  sletric  27726  muls0ord  28128  tgbtwnconn1  28500  legov3  28523  coltr  28572  colline  28574  tglowdim2ln  28576  ragflat3  28631  ragperp  28642  lmieu  28709  lmicom  28713  lmimid  28719  numedglnl  29069  pthisspthorcycl  29730  nvmul0or  30577  hvmul0or  30952  atomli  32309  atordi  32311  iundisj2f  32517  iundisj2fi  32720  chnind  32937  gsumfs2d  32995  mxidlprm  33431  ssmxidl  33435  qsdrng  33458  zarclssn  33850  signsply0  34529  cvmsdisj  35238  nepss  35681  dfon2lem6  35752  btwnconn1lem13  36063  wl-exeq  37498  eqvreldisj  38578  lsator0sp  38965  lkreqN  39134  2at0mat0  39490  trlator0  40136  dochkrshp4  41354  dochsat0  41422  lcfl6  41465  expeqidd  42321  rp-fakeimass  43483  frege124d  43732  clsk1independent  44017  mnringmulrcld  44200  pm10.57  44343  icccncfext  45864  fourierdlem70  46153  ichnreuop  47434  uzlidlring  48158  nneop  48454  mo0sn  48742  euendfunc2  49360