Theorem ori 375

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

Hypothesis

Ref	Expression
ori.1

Assertion

Ref	Expression
ori

Proof of Theorem ori

Step	Hyp	Ref	Expression
1		ori.1	. 2
2		df-or 370	. 2
3	1, 2	mpbi 208	1

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

This theorem is referenced by:  3ori  1288  mtpor  1603  exmoeu  2316  moanim  2350  moexex  2363  mo2icl  3278  mosubopt  4750  fvrn0  5893  eliman0  5900  dff3  6044  onuninsuci  6675  omelon2  6712  infensuc  7715  rankxpsuc  8321  cardlim  8374  alephreg  8978  tskcard  9180  sinhalfpilem  22856  sltres  29424

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