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  1913  axi12  2730  r19.30  3129  sspss  4029  eqoreldif  4642  sssn  4781  pwpw0  4830  unissint  4931  disjiund  5093  disjxiun  5099  otsndisj  5491  otiunsndisj  5492  pwssun  5542  isso2i  5595  ordtr3  6409  ordtri2or  6463  unizlim  6487  fvclss  7246  orduniorsuc  7842  ordzsl  7857  nn0suc  7907  xpexr  7931  soseq  8179  odi  8591  swoso  8756  erdisj  8779  ordtypelem7  9522  wemapsolem  9548  domwdom  9572  iscard3  10176  ackbij1lem18  10318  fin56  10475  entric  10645  gchdomtri  10718  inttsk  10863  r1tskina  10871  psslinpr  11120  1re  11312  ssxr  11383  letric  11414  mul0or  11960  mulge0b  12191  zeo  12789  uzm1  13003  xrletri  13286  supxrgtmnf  13463  sq01  14373  ruclem3  16407  prm2orodd  16872  phiprmpw  16959  pleval2i  18514  chnind  18801  irredn0  20659  lvecvs0or  21392  lssvs0or  21394  lspsnat  21429  lsppratlem1  21431  domnchr  21844  fctop  23328  cctop  23330  ppttop  23331  clslp  23472  restntr  23506  cnconn  23746  txindis  23959  txconn  24014  isufil2  24233  ufprim  24234  alexsubALTlem3  24374  pmltpc  25777  iundisj2  25876  limcco  26219  fta1b  26496  aalioulem2  26666  abelthlem2  26765  logreclem  27096  dchrfi  27588  2sqb  27765  nosepdmlem  28046  noetasuplem4  28099  lestric  28131  muls0ord  28577  bdayfinbndlem1  28859  tgbtwnconn1  29044  legov3  29067  coltr  29122  colline  29124  tglowdim2ln  29126  ragflat3  29187  ragperp  29198  lmieu  29295  lmicom  29299  lmimid  29305  numedglnl  29728  pthisspthorcycl  30396  nvmul0or  31258  hvmul0or  31633  atomli  32990  atordi  32992  tgextalem1inag  33076  iundisj2f  33232  iundisj2fi  33436  gsumfs2d  33669  mxidlprm  34042  ssmxidl  34046  qsdrng  34068  dflringlem3  34075  dflring4  34077  zarclssn  34552  signsply0  35227  cvmsdisj  36122  nepss  36576  dfon2lem6  36643  btwnconn1lem13  36957  wl-exeq  38560  eqvreldisj  39724  lsator0sp  40152  lkreqN  40321  2at0mat0  40676  trlator0  41322  dochkrshp4  42540  dochsat0  42608  lcfl6  42651  expeqidd  43476  sn-remul0ord  43553  rp-fakeimass  44607  frege124d  44855  clsk1independent  45140  mnringmulrcld  45320  pm10.57  45449  icccncfext  46991  fourierdlem70  47280  ichnreuop  48648  uzlidlring  49426  nneop  49732  mo0sn  50021  euendfunc2  50756  parhomeqor2  50852  parhomeqor  50853