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  1916  axi12  2733  r19.30  3133  sspss  4032  eqoreldif  4646  sssn  4785  pwpw0  4834  unissint  4935  disjiund  5097  disjxiun  5103  otsndisj  5497  otiunsndisj  5498  pwssun  5548  isso2i  5601  ordtr3  6430  ordtri2or  6484  unizlim  6508  fvclss  7271  orduniorsuc  7868  ordzsl  7883  nn0suc  7933  xpexr  7957  soseq  8206  odi  8618  swoso  8783  erdisj  8806  ordtypelem7  9548  wemapsolem  9574  domwdom  9598  iscard3  10202  ackbij1lem18  10344  fin56  10501  entric  10671  gchdomtri  10744  inttsk  10889  r1tskina  10897  psslinpr  11146  1re  11338  ssxr  11409  letric  11440  mul0or  11986  mulge0b  12217  zeo  12815  uzm1  13029  xrletri  13312  supxrgtmnf  13489  sq01  14399  ruclem3  16433  prm2orodd  16898  phiprmpw  16985  pleval2i  18540  chnind  18827  irredn0  20686  lvecvs0or  21419  lssvs0or  21421  lspsnat  21456  lsppratlem1  21458  domnchr  21871  fctop  23355  cctop  23357  ppttop  23358  clslp  23499  restntr  23533  cnconn  23773  txindis  23986  txconn  24041  isufil2  24260  ufprim  24261  alexsubALTlem3  24401  pmltpc  25804  iundisj2  25903  limcco  26246  fta1b  26523  aalioulem2  26693  abelthlem2  26792  logreclem  27123  dchrfi  27615  2sqb  27792  nosepdmlem  28073  noetasuplem4  28126  lestric  28158  muls0ord  28604  bdayfinbndlem1  28886  tgbtwnconn1  29071  legov3  29094  coltr  29149  colline  29151  tglowdim2ln  29153  ragflat3  29214  ragperp  29225  lmieu  29322  lmicom  29326  lmimid  29332  numedglnl  29755  pthisspthorcycl  30423  nvmul0or  31285  hvmul0or  31660  atomli  33017  atordi  33019  tgextalem1inag  33103  iundisj2f  33259  iundisj2fi  33462  gsumfs2d  33698  zzedom  33939  mxidlprm  34079  ssmxidl  34083  qsdrng  34105  dflringlem3  34112  dflring4  34114  zarclssn  34588  signsply0  35263  cvmsdisj  36215  nepss  36674  dfon2lem6  36741  btwnconn1lem13  37055  wl-exeq  38671  eqvreldisj  39833  lsator0sp  40261  lkreqN  40430  2at0mat0  40785  trlator0  41431  dochkrshp4  42649  dochsat0  42717  lcfl6  42760  expeqidd  43586  sn-remul0ord  43663  rp-fakeimass  44716  frege124d  44964  clsk1independent  45249  mnringmulrcld  45429  pm10.57  45558  icccncfext  47112  fourierdlem70  47401  ichnreuop  48769  uzlidlring  49547  nneop  49853  mo0sn  50142  euendfunc2  50877  parhomeqor2  50973  parhomeqor  50974