orrd - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > orrd		Unicode version

Theorem orrd 367

Description: Deduce implication from disjunction. (Contributed by NM, 27-Nov-1995.)

**Hypothesis**
Ref	Expression
orrd.1

**Assertion**
Ref	Expression
orrd	$\/$

**Proof of Theorem orrd**
Step	Hyp	Ref	Expression
1		orrd.1	. 2
2		pm2.54 363	. 2 $\/$
3	1, 2	syl 15	1 $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 357

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

This theorem depends on definitions: df-bi 177 df-or 359

This theorem is referenced by: olc 373 orc 374 pm2.68 399 pm4.79 566 sspss 3368 pwpw0 3855 sssn 3864 pwsnALT 3882 unissint 3950 pwadjoin 4119 nndisjeq 4429 xpexr 5109 fvclss 5462 erdisj 5972