New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3adant1 | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
3adant.1 | ⊢ ((φ ∧ ψ) → χ) |
Ref | Expression |
---|---|
3adant1 | ⊢ ((θ ∧ φ ∧ ψ) → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpc 954 | . 2 ⊢ ((θ ∧ φ ∧ ψ) → (φ ∧ ψ)) | |
2 | 3adant.1 | . 2 ⊢ ((φ ∧ ψ) → χ) | |
3 | 1, 2 | syl 15 | 1 ⊢ ((θ ∧ φ ∧ ψ) → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 ∧ w3a 934 |
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-an 360 df-3an 936 |
This theorem is referenced by: 3ad2ant2 977 3ad2ant3 978 rsp2e 2677 sbciegft 3076 otkelins2kg 4253 otkelins3kg 4254 nnsucelr 4428 nndisjeq 4429 leltfintr 4458 ltfintr 4459 ncfinlower 4483 tfin11 4493 sfindbl 4530 vfinncvntnn 4548 fununiq 5517 mpt2eq3ia 5670 clos1basesuc 5882 enadj 6060 lectr 6211 leltctr 6212 lecponc 6213 taddc 6228 letc 6230 ce2le 6232 addcdi 6249 addcdir 6250 ncslemuc 6254 nchoicelem17 6303 |
Copyright terms: Public domain | W3C validator |