Theorem ord 675

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.8  756  orcanai  870  ax-12  1442  swopo  4061  sotritrieq  4080  suc11g  4300  ordsoexmid  4305  nnsuc  4356  sotri2  4742  nnsucsssuc  6094  nntri2  6096  nntri1  6097  nnsseleq  6102  elni2  6504  nlt1pig  6531  nngt1ne1  8073  zleloe  8398  zapne  8422  nneo  8450  zeo2  8453  fzocatel  9208  bj-peano4  10750