Theorem ori 390

Description: Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)

Hypothesis

Ref	Expression
ori.1	|- ( ph \/ ps )

Assertion

Ref	Expression
ori	|- ( -. ph -> ps )

Proof of Theorem ori

Step	Hyp	Ref	Expression
1		ori.1	. 2 |- ( ph \/ ps )
2		df-or 385	. 2 |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
3	1, 2	mpbi 220	1 |- ( -. ph -> ps )

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

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 197  df-or 385

This theorem is referenced by:  3ori  1388  mtpor  1695  exmoeu  2502  moanim  2529  moexex  2541  mo2icl  3385  mosubopt  4972  fvrn0  6216  eliman0  6223  dff3  6372  onuninsuci  7040  omelon2  7077  infensuc  8138  rankxpsuc  8745  cardlim  8798  alephreg  9404  tskcard  9603  sinhalfpilem  24215  sltres  31815