New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3adant3 | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
3adant.1 | ⊢ ((φ ∧ ψ) → χ) |
Ref | Expression |
---|---|
3adant3 | ⊢ ((φ ∧ ψ ∧ θ) → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa 952 | . 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-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: vtoclgft 2905 eqeu 3007 sikss1c1c 4267 ins2kss 4279 ins3kss 4280 leltfintr 4458 ltfintr 4459 lefinlteq 4463 ltfintri 4466 ncfineleq 4477 tfindi 4496 tfinltfin 4501 sfintfin 4532 tfinnn 4534 spfinsfincl 4539 addccan2 4559 brsi 4761 fnco 5191 resdif 5306 fnimapr 5374 f1ocnvfvb 5479 f1oiso2 5500 fununiq 5517 ovig 5597 ov2ag 5598 ov6g 5600 ovg 5601 ovmpt2x 5712 elmapg 6012 elpmg 6013 ceclr 6187 addlec 6208 lectr 6211 leaddc1 6214 nclenn 6249 addcdir 6251 lemuc1 6253 ncslemuc 6255 lecadd2 6266 spaccl 6286 |
Copyright terms: Public domain | W3C validator |