New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > orrd | GIF version |
Description: Deduce implication from disjunction. (Contributed by NM, 27-Nov-1995.) |
Ref | Expression |
---|---|
orrd.1 | ⊢ (φ → (¬ ψ → χ)) |
Ref | Expression |
---|---|
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 |
Copyright terms: Public domain | W3C validator |