Theorem ord 729

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)

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		pm2.53 727	. 2 |- ( ( ps \/ ch ) -> ( -. ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( -. ps -> ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  815  orcanai  933  ax12  1558  swopo  4397  sotritrieq  4416  suc11g  4649  ordsoexmid  4654  nnsuc  4708  sotri2  5126  nnsucsssuc  6638  nntri2  6640  nntri1  6642  nnsseleq  6647  djulclb  7222  0ct  7274  exmidomniim  7308  omniwomnimkv  7334  elni2  7501  nlt1pig  7528  nngt1ne1  9145  zleloe  9493  zapne  9521  nneo  9550  zeo2  9553  fzocatel  10405  seqf1oglem1  10741  seqf1oglem2  10742  bitsinv1lem  12472  dfphi2  12742  prmdiv  12757  odzdvds  12768  pc2dvds  12853  fldivp1  12871  pcfac  12873  1arith  12890  4sqlem10  12910  plyaddlem1  15421  plymullem1  15422  gausslemma2dlem4  15743  lgseisenlem1  15749  bj-peano4  16318