Theorem ord 377

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

Hypothesis

Ref	Expression
ord.1	|- ( ph -> ( ps \/ ch ) )

Assertion

Ref	Expression
ord	|- ( ph -> ( -. ps -> ch ) )

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 |- ( ph -> ( ps \/ ch ) )
2		df-or 370	. 2 |- ( ( ps \/ ch ) <-> ( -. ps -> ch ) )
3	1, 2	sylib 196	1 |- ( ph -> ( -. ps -> ch ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  orcanai  897  oplem1  948  ecase23d  1315  19.33b  1662  elpwunsn  3905  eqsn  4022  disji2  4267  disjxiun  4277  pwssun  4614  swopo  4638  somo  4662  ordtri3or  4738  ordtri1  4739  ordtri3  4742  ord0eln0  4760  suc11  4809  frsn  4896  foconst  5619  ordeleqon  6389  ssonprc  6392  onmindif2  6412  limsssuc  6450  limom  6480  onfununi  6788  oeeulem  7028  uniinqs  7168  pw2f1olem  7403  pssnn  7519  ordtypelem9  7728  ordtypelem10  7729  oismo  7742  preleq  7811  suc11reg  7813  cantnfp1lem2  7875  cantnflem1  7885  cantnfp1lem2OLD  7901  cantnflem1OLD  7908  cnfcom2lem  7922  cnfcom3lem  7924  cnfcom2lemOLD  7930  cnfcom3lemOLD  7932  rankxpsuc  8077  cardlim  8130  alephdom  8239  cardaleph  8247  iscard3  8251  pwcdadom  8373  cfslbn  8424  fin1a2lem12  8568  gchi  8778  fpwwe2lem13  8796  tskssel  8911  inttsk  8928  inar1  8929  r1tskina  8936  tskuni  8937  gruina  8972  grur1  8974  nlt1pi  9062  nqereu  9085  leltne  9451  nneo  10712  zeo2  10715  xrleltne  11109  nltpnft  11125  ngtmnft  11126  xrrebnd  11127  xaddf  11181  xrsupsslem  11256  xrinfmsslem  11257  seqf1olem1  11828  seqf1olem2  11829  discr1  11983  hashnncl  12117  seqcoll2  12200  sqeqd  12638  sqrmo  12724  isercoll  13128  dvdseq  13562  bitsfzo  13613  bitsinv1lem  13619  bitsf1  13624  bezoutlem3  13706  eucalglt  13742  phibndlem  13827  dfphi2  13831  prmdiv  13842  odzdvds  13849  pceq0  13919  pc2dvds  13927  fldivp1  13941  pcfac  13943  prmreclem3  13961  1arith  13970  4sqlem10  13990  4sqlem17  14004  4sqlem18  14005  vdwlem6  14029  ramubcl  14061  ramcl  14072  mrissmrcd  14560  psgnunilem5  15979  oddvdsnn0  16026  odnncl  16027  oddvds  16029  odcl2  16045  gexdvds  16062  gexnnod  16066  sylow1lem1  16076  odcau  16082  pgpssslw  16092  efgs1b  16212  efgredlema  16216  torsubg  16315  prmcyg  16349  gsumval3eu  16360  ablfacrplem  16539  ablfac1eu  16547  lspdisj  17127  lspsncv0  17148  fidomndrnglem  17299  gzrngunitlem  17720  prmirredlem  17758  prmirredlemOLD  17761  fctop  18449  cctop  18451  ppttop  18452  pptbas  18453  ordtrest2lem  18648  conclo  18860  txindis  19048  filcon  19297  ufilb  19320  cldsubg  19522  reconnlem1  20244  reconnlem2  20245  metds0  20267  metdseq0  20271  metnrmlem1a  20275  iccpnfhmeo  20358  xrhmeo  20359  cphsubrglem  20537  minveclem3b  20756  minveclem4a  20758  vitalilem4  20932  itg2gt0  21079  itgsplitioo  21156  limccnp2  21208  rollelem  21302  dvlip  21306  itgsubstlem  21361  plyaddlem1  21565  plymullem1  21566  coefv0  21599  dgreq0  21616  radcnv0  21765  pserdvlem2  21777  pilem2  21801  sineq0  21867  logtayl  21989  cxpsqr  22032  isosctrlem2  22101  atantayl2  22217  leibpilem1  22219  rlimcnp2  22244  amgm  22268  basellem3  22304  muval2  22356  sqf11  22361  ppinprm  22374  chtnprm  22376  perfectlem2  22453  lgsdir  22553  lgsabs1  22557  lgseisenlem1  22572  2sqlem7  22593  2sqblem  22600  chebbnd1lem1  22602  dchrisum0flblem1  22641  pntpbnd1  22719  pntpbnd2  22720  ostth  22772  minvecolem5  24104  staddi  25472  stadd3i  25474  atsseq  25573  atom1d  25579  atoml2i  25609  disji2f  25744  disjif2  25748  ordtrest2NEWlem  26205  eulerpartlemb  26598  subfacp1lem6  26920  cvmscld  27009  cvmsss2  27010  cvmseu  27012  ordtoplem  28128  ordcmp  28140  heiborlem6  28556  isfldidl  28709  pridlc2  28713  ctbnfien  28999  pw2f1ocnv  29228  unxpwdom3  29290  dgrsub2  29333  fmul01lt1lem1  29607  stoweidlem35  29673  stirlinglem5  29716  stirlinglem12  29723  lsatcmp  32218  lsatcmp2  32219  2atm  32741  trlatn0  33386  trlval3  33401  cdleme18c  33507  cdlemg17b  33876  cdlemg17i  33883  cdlemh  34031  dia2dimlem2  34280  dia2dimlem3  34281  dochlkr  34600  dochkrshp  34601  lcfl6  34715  lcfrlem9  34765  hdmap14lem6  35091  hgmapval0  35110