Theorem ord 878

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)

Hypothesis

Ref	Expression
ord.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
ord	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		df-or 862	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒))
3	1, 2	sylib 221	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:  olcnd  891  orcanai  1018  ecase2d  1047  oplem1  1072  ornld  1077  19.33b  1918  elpwunsn  4652  disji2  5095  disjxiun  5108  pwssun  5555  swopo  5582  sotric  5601  sotrieq  5602  somo  5610  ordtri3or  6397  ordtri1  6398  suc11  6474  foconst  6811  ordeleqon  7787  ssonprc  7792  onmindif2  7812  limsssuc  7852  limom  7884  onfununi  8334  oeeulem  8593  uniinqs  8801  pw2f1olem  9076  pssnn  9160  ordtypelem9  9495  ordtypelem10  9496  oismo  9509  preleqALT  9593  suc11reg  9595  cantnfp1lem2  9655  cantnflem1  9665  cnfcom2lem  9677  cnfcom3lem  9679  rankxpsuc  9861  cardlim  9974  alephdom  10081  cardaleph  10089  iscard3  10093  pwdjudom  10214  cfslbn  10266  fin1a2lem12  10410  gchi  10628  tskssel  10761  inttsk  10778  inar1  10779  r1tskina  10786  tskuni  10787  gruina  10822  grur1  10824  nlt1pi  10910  nqereu  10933  leltne  11318  nneo  12700  zeo2  12703  xrleltne  13190  nltpnft  13210  ngtmnft  13212  xrrebnd  13214  xaddf  13270  xrsupsslem  13353  xrinfmsslem  13354  fzocatel  13779  seqf1olem1  14099  seqf1olem2  14100  znsqcld  14220  discr1  14297  hashnncl  14424  seqcoll2  14524  sgn3da  15166  sqeqd  15245  sqrmo  15330  isercoll  15747  bitsfzo  16519  bitsinv1lem  16525  bitsf1  16530  bezoutlem3  16625  eucalglt  16669  phibndlem  16855  dfphi2  16859  prmdiv  16870  odzdvds  16881  pceq0  16957  pc2dvds  16965  fldivp1  16983  pcfac  16985  prmreclem3  17004  1arith  17013  4sqlem10  17033  4sqlem17  17047  4sqlem18  17048  vdwlem6  17072  ramubcl  17104  ramcl  17115  mrissmrcd  17722  psgnunilem5  19612  oddvdsnn0  19662  odnncl  19663  oddvds  19665  odcl2  19683  gexdvds  19702  gexnnod  19706  sylow1lem1  19716  odcau  19722  pgpssslw  19732  efgs1b  19854  efgredlema  19858  torsubg  19972  prmcyg  20012  gsumval3eu  20022  ablfacrplem  20185  ablfac1eu  20193  ablsimpgprmd  20235  fidomndrnglem  20930  lspdisj  21303  lspsncv0  21324  prmidlc2  21528  gzrngunitlem  21636  prmirredlem  21676  fctop  23215  cctop  23217  ppttop  23218  pptbas  23219  ordtrest2lem  23414  connclo  23626  txindis  23846  filconn  24095  ufilb  24118  cldsubg  24323  reconnlem1  25039  reconnlem2  25040  metds0  25063  metdseq0  25067  metnrmlem1a  25071  iccpnfhmeo  25159  xrhmeo  25160  cphsubrglem  25391  minveclem3b  25642  minveclem4a  25644  vitalilem4  25825  itg2gt0  25974  itgsplitioo  26052  limccnp2  26106  rollelem  26203  dvlip  26207  itgsubstlem  26262  plyaddlem1  26425  plymullem1  26426  coefv0  26460  dgreq0  26477  radcnv0  26634  pserdvlem2  26646  pilem2  26670  sineq0  26744  logtayl  26880  cxpsqrt  26923  isosctrlem2  27039  atantayl2  27158  rlimcnp2  27186  amgm  27210  basellem3  27302  muval2  27353  sqf11  27358  ppinprm  27371  chtnprm  27373  perfectlem2  27449  lgsdir  27551  lgsabs1  27555  lgseisenlem1  27594  2sqlem7  27643  2sqblem  27650  2sqmod  27655  2sqreultblem  27667  2sqreunnltblem  27670  chebbnd1lem1  27688  dchrisum0flblem1  27727  pntpbnd1  27805  pntpbnd2  27806  ostth  27858  nosepon  27884  abssge0  28493  elnns2  28589  dfnns2  28620  z12bday  28733  symquadlem  29021  midexlem  29024  colperp  29065  midex  29073  oppperpex  29089  hlpasch  29093  hpgerlem  29102  colopp  29106  plngrotlem1  29124  lmieu  29148  lmicom  29152  trgcopy  29170  cgracol  29194  minvecolem5  31308  staddi  32673  stadd3i  32675  atsseq  32774  atom1d  32780  atoml2i  32810  disji2f  32997  disjif2  33001  fprodex01  33243  psgnfzto1stlem  33488  lvecdim0  34065  ordtrest2NEWlem  34380  eulerpartlemb  34827  subfacp1lem6  35718  cvmscld  35806  cvmsss2  35807  cvmseu  35809  ordtoplem  37007  ordcmp  37019  poimirlem25  38357  heiborlem6  38529  isfldidl  38781  pridlc2  38785  mpobi123f  38873  mptbi12f  38877  ac6s6  38883  lsatcmp  39839  lsatcmp2  39840  2atm  40363  trlatn0  41008  trlval3  41023  cdleme18c  41129  cdlemg17b  41498  cdlemg17i  41505  cdlemh  41653  dia2dimlem2  41901  dia2dimlem3  41902  dochlkr  42221  dochkrshp  42222  lcfl6  42336  lcfrlem9  42386  hdmap14lem6  42709  hgmapval0  42728  ioin9i8  43038  ctbnfien  43622  pw2f1ocnv  43841  unxpwdom3  43899  dgrsub2  43939  dflim5  44133  rp-fakeanorass  44316  mnuprdlem1  45059  mnuprdlem2  45060  mnurndlem1  45068  disjxp1  45866  fmul01lt1lem1  46377  stoweidlem35  46826  stirlinglem5  46869  stirlinglem12  46876  fourierdlem42  46940  fourierdlem93  46990  perfectALTVlem2  48564