Theorem orrd 392

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

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

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 196  df-or 384

This theorem is referenced by:  olc  398  orc  399  pm2.68  425  pm4.79  605  19.30  1798  axi12  2588  axbnd  2589  sspss  3668  eqoreldif  4172  pwpw0  4284  sssn  4298  pwsnALT  4367  unissint  4436  disjxiun  4579  disjxiunOLD  4580  otsndisj  4904  otiunsndisj  4905  pwssun  4944  isso2i  4991  ordtr3  5686  ordtr3OLD  5687  ordtri2or  5739  unizlim  5761  fvclss  6404  orduniorsuc  6922  ordzsl  6937  nn0suc  6982  xpexr  6999  odi  7546  swoso  7662  erdisj  7681  ordtypelem7  8312  wemapsolem  8338  domwdom  8362  iscard3  8799  ackbij1lem18  8942  fin56  9098  entric  9258  gchdomtri  9330  inttsk  9475  r1tskina  9483  psslinpr  9732  ssxr  9986  letric  10016  mul0or  10546  mulge0b  10772  zeo  11339  uzm1  11594  xrletri  11860  supxrgtmnf  12031  sq01  12848  ruclem3  14801  prm2orodd  15242  phiprmpw  15319  pleval2i  16787  irredn0  18526  drngmul0or  18591  lvecvs0or  18929  lssvs0or  18931  lspsnat  18966  lsppratlem1  18968  domnchr  19699  fctop  20618  cctop  20620  ppttop  20621  clslp  20762  restntr  20796  cnconn  21035  txindis  21247  txcon  21302  isufil2  21522  ufprim  21523  alexsubALTlem3  21663  pmltpc  23026  iundisj2  23124  limcco  23463  fta1b  23733  aalioulem2  23892  abelthlem2  23990  logreclem  24300  dchrfi  24780  2sqb  24957  tgbtwnconn1  25270  legov3  25293  coltr  25342  colline  25344  tglowdim2ln  25346  ragflat3  25401  ragperp  25412  lmieu  25476  lmicom  25480  lmimid  25486  nvmul0or  26889  hvmul0or  27266  atomli  28625  atordi  28627  iundisj2f  28785  iundisj2fi  28943  signsply0  29954  cvmsdisj  30506  nepss  30854  dfon2lem6  30937  soseq  30995  btwnconn1lem13  31376  wl-exeq  32500  lsator0sp  33306  lkreqN  33475  2at0mat0  33829  trlator0  34476  dochkrshp4  35696  dochsat0  35764  lcfl6  35807  rp-fakeimass  36876  frege124d  37072  clsk1independent  37364  pm10.57  37592  icccncfext  38773  fourierdlem70  39069  uzlidlring  41719  nneop  42114