New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > adantld | GIF version |
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.) |
Ref | Expression |
---|---|
adantld.1 | ⊢ (φ → (ψ → χ)) |
Ref | Expression |
---|---|
adantld | ⊢ (φ → ((θ ∧ ψ) → χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 447 | . 2 ⊢ ((θ ∧ ψ) → ψ) | |
2 | adantld.1 | . 2 ⊢ (φ → (ψ → χ)) | |
3 | 1, 2 | syl5 28 | 1 ⊢ (φ → ((θ ∧ ψ) → χ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
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 177 df-an 360 |
This theorem is referenced by: jaoa 496 dedlema 920 dedlemb 921 prlem1 928 spimed 1977 equveli 1988 2eu3 2286 unineq 3505 tfinpw1 4494 tfinltfinlem1 4500 sfinltfin 4535 spfinsfincl 4539 vfinspsslem1 4550 clos1conn 5879 taddc 6229 nchoicelem12 6300 |
Copyright terms: Public domain | W3C validator |