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 6229 letc 6231 ce2le 6233 addcdi 6250 addcdir 6251 ncslemuc 6255 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |