Theorem orrd 869

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

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

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 208  df-or 854

This theorem is referenced by:  orc  873  olc  874  pm2.68  906  pm4.79  1011  19.30  1888  axi12  2710  r19.30  3107  sspss  4040  eqoreldif  4624  pwpw0  4751  sssn  4764  unissint  4909  disjiund  5070  disjxiun  5076  otsndisj  5467  otiunsndisj  5468  pwssun  5517  isso2i  5570  ordtr3  6363  ordtri2or  6417  unizlim  6441  fvclss  7192  orduniorsuc  7777  ordzsl  7792  nn0suc  7841  xpexr  7865  soseq  8106  odi  8511  swoso  8675  erdisj  8698  ordtypelem7  9436  wemapsolem  9462  domwdom  9486  iscard3  10013  ackbij1lem18  10156  fin56  10313  entric  10477  gchdomtri  10550  inttsk  10695  r1tskina  10703  psslinpr  10952  1re  11142  ssxr  11213  letric  11244  mul0or  11788  mulge0b  12024  zeo  12613  uzm1  12820  xrletri  13102  supxrgtmnf  13279  sq01  14185  ruclem3  16198  prm2orodd  16658  phiprmpw  16744  pleval2i  18298  chnind  18585  irredn0  20401  drngmul0orOLD  20740  lvecvs0or  21108  lssvs0or  21110  lspsnat  21145  lsppratlem1  21147  domnchr  21514  fctop  22994  cctop  22996  ppttop  22997  clslp  23138  restntr  23172  cnconn  23412  txindis  23624  txconn  23679  isufil2  23898  ufprim  23899  alexsubALTlem3  24039  pmltpc  25442  iundisj2  25541  limcco  25885  fta1b  26162  aalioulem2  26324  abelthlem2  26422  logreclem  26751  dchrfi  27243  2sqb  27420  nosepdmlem  27672  noetasuplem4  27725  lestric  27757  muls0ord  28202  bdayfinbndlem1  28484  tgbtwnconn1  28668  legov3  28691  coltr  28740  colline  28742  tglowdim2ln  28744  ragflat3  28799  ragperp  28810  lmieu  28877  lmicom  28881  lmimid  28887  numedglnl  29238  pthisspthorcycl  29895  nvmul0or  30746  hvmul0or  31121  atomli  32478  atordi  32480  iundisj2f  32686  iundisj2fi  32896  gsumfs2d  33149  mxidlprm  33560  ssmxidl  33564  qsdrng  33587  zarclssn  34064  signsply0  34742  cvmsdisj  35505  nepss  35953  dfon2lem6  36021  btwnconn1lem13  36334  wl-exeq  37912  eqvreldisj  39072  lsator0sp  39500  lkreqN  39669  2at0mat0  40024  trlator0  40670  dochkrshp4  41888  dochsat0  41956  lcfl6  41999  expeqidd  42809  sn-remul0ord  42892  rp-fakeimass  43963  frege124d  44212  clsk1independent  44497  mnringmulrcld  44679  pm10.57  44822  icccncfext  46337  fourierdlem70  46626  ichnreuop  47954  uzlidlring  48733  nneop  49024  mo0sn  49313  euendfunc2  50024