![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp2ll | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp2ll | ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll 757 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant2 1125 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: tfrlem5 7759 omeu 7949 4sqlem18 16070 vdwlem10 16098 0catg 16733 mvrf1 19822 mdetuni0 20832 mdetmul 20834 tsmsxp 22366 ax5seglem3 26280 btwnconn1lem1 32783 btwnconn1lem2 32784 btwnconn1lem3 32785 btwnconn1lem12 32794 btwnconn1lem13 32795 lshpkrlem6 35271 athgt 35612 2llnjN 35723 dalaw 36042 lhpmcvr4N 36182 cdlemb2 36197 4atexlemex6 36230 cdlemd7 36360 cdleme01N 36377 cdleme02N 36378 cdleme0ex1N 36379 cdleme0ex2N 36380 cdleme7aa 36398 cdleme7c 36401 cdleme7d 36402 cdleme7e 36403 cdleme7ga 36404 cdleme7 36405 cdleme11a 36416 cdleme20k 36475 cdleme27cl 36522 cdleme42e 36635 cdleme42h 36638 cdleme42i 36639 cdlemf 36719 cdlemg2kq 36758 cdlemg2m 36760 cdlemg8a 36783 cdlemg11aq 36794 cdlemg10c 36795 cdlemg11b 36798 cdlemg17a 36817 cdlemg31b0N 36850 cdlemg31c 36855 cdlemg33c0 36858 cdlemg41 36874 cdlemh2 36972 cdlemn9 37361 dihglbcpreN 37456 dihmeetlem3N 37461 dihmeetlem13N 37475 pellex 38363 expmordi 38475 |
Copyright terms: Public domain | W3C validator |