imorri - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imorri		Unicode version

Theorem imorri 414

Description: Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

**Hypothesis**
Ref	Expression
imorri.1

**Assertion**
Ref	Expression
imorri

**Proof of Theorem imorri**
Step	Hyp	Ref	Expression
1		imorri.1	. 2
2		imor 412	. 2
3	1, 2	mpbir 209	1

Colors of variables: wff setvar class

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

This theorem is referenced by: anmp 1584 meran2 29877 meran3 29878

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