Theorem orrd 874

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

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

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 209  df-or 859

This theorem is referenced by:  orc  878  olc  879  pm2.68  911  pm4.79  1016  19.30  1900  axi12  2731  r19.30  3128  sspss  4053  eqoreldif  4641  pwpw0  4768  sssn  4781  unissint  4927  disjiund  5088  disjxiun  5094  otsndisj  5485  otiunsndisj  5486  pwssun  5535  isso2i  5588  ordtr3  6386  ordtri2or  6440  unizlim  6464  fvclss  7219  orduniorsuc  7804  ordzsl  7819  nn0suc  7869  xpexr  7893  soseq  8132  odi  8541  swoso  8706  erdisj  8729  ordtypelem7  9465  wemapsolem  9491  domwdom  9515  iscard3  10042  ackbij1lem18  10185  fin56  10343  entric  10507  gchdomtri  10580  inttsk  10725  r1tskina  10733  psslinpr  10982  1re  11174  ssxr  11245  letric  11276  mul0or  11820  mulge0b  12055  zeo  12652  uzm1  12866  xrletri  13148  supxrgtmnf  13325  sq01  14231  ruclem3  16255  prm2orodd  16715  phiprmpw  16801  pleval2i  18356  chnind  18643  irredn0  20458  drngmul0orOLD  20797  lvecvs0or  21165  lssvs0or  21167  lspsnat  21202  lsppratlem1  21204  domnchr  21571  fctop  23051  cctop  23053  ppttop  23054  clslp  23195  restntr  23229  cnconn  23469  txindis  23681  txconn  23736  isufil2  23955  ufprim  23956  alexsubALTlem3  24096  pmltpc  25499  iundisj2  25598  limcco  25942  fta1b  26219  aalioulem2  26384  abelthlem2  26482  logreclem  26814  dchrfi  27306  2sqb  27483  nosepdmlem  27734  noetasuplem4  27787  lestric  27819  muls0ord  28265  bdayfinbndlem1  28547  tgbtwnconn1  28731  legov3  28754  coltr  28803  colline  28805  tglowdim2ln  28807  ragflat3  28862  ragperp  28873  lmieu  28940  lmicom  28944  lmimid  28950  numedglnl  29301  pthisspthorcycl  29958  nvmul0or  30809  hvmul0or  31184  atomli  32541  atordi  32543  iundisj2f  32749  iundisj2fi  32959  gsumfs2d  33201  mxidlprm  33618  ssmxidl  33622  qsdrng  33645  dflringlem3  33652  dflring4  33654  zarclssn  34130  signsply0  34805  cvmsdisj  35580  nepss  36028  dfon2lem6  36096  btwnconn1lem13  36409  wl-exeq  37997  eqvreldisj  39157  lsator0sp  39585  lkreqN  39754  2at0mat0  40109  trlator0  40755  dochkrshp4  41973  dochsat0  42041  lcfl6  42084  expeqidd  42894  sn-remul0ord  42977  rp-fakeimass  44048  frege124d  44297  clsk1independent  44582  mnringmulrcld  44764  pm10.57  44907  icccncfext  46421  fourierdlem70  46710  ichnreuop  48038  uzlidlring  48817  nneop  49108  mo0sn  49397  euendfunc2  50108