Theorem ord 732

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

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

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 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  818  orcanai  936  ax12  1561  swopo  4409  sotritrieq  4428  suc11g  4661  ordsoexmid  4666  nnsuc  4720  sotri2  5141  nnsucsssuc  6703  nntri2  6705  nntri1  6707  nnsseleq  6712  djulclb  7314  0ct  7366  exmidomniim  7400  omniwomnimkv  7426  elni2  7594  nlt1pig  7621  nngt1ne1  9237  zleloe  9587  zapne  9615  nneo  9644  zeo2  9647  fzocatel  10507  seqf1oglem1  10844  seqf1oglem2  10845  bitsinv1lem  12602  dfphi2  12872  prmdiv  12887  odzdvds  12898  pc2dvds  12983  fldivp1  13001  pcfac  13003  1arith  13020  4sqlem10  13040  plyaddlem1  15558  plymullem1  15559  gausslemma2dlem4  15883  lgseisenlem1  15889  bj-peano4  16671