Theorem ori 247

Description: Infer implication from disjunction.

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 241	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	mpbi 206	1 |- (-. ph -> ps)

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239

This theorem is referenced by:  3ori 1157  moexex 1841  mo2icl 2434  mosubopt 3551  onuninsuci 3921  dff3 4790  omelon 5736  rankxpsuc 5826  cardom 5872  omsubel 5883  brdom3 5963  cardlim 6003  unialeph 6043  nneoi 7409  bcpasci 8221  sinhalfpilem 10028  bnj27 12390  fz1eqblem 13608  axfelem12 14042  mof 14160  omsubelOLD 15392

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241

Copyright terms: Public domain