![]() |
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 766 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant2 1132 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 206 df-an 396 df-3an 1087 |
This theorem is referenced by: tfrlem5 8401 omeu 8606 expmordi 14164 4sqlem18 16931 vdwlem10 16959 0catg 17668 mvrf1 21928 mdetuni0 22536 mdetmul 22538 tsmsxp 24072 ax5seglem3 28755 btwnconn1lem1 35683 btwnconn1lem2 35684 btwnconn1lem3 35685 btwnconn1lem12 35694 btwnconn1lem13 35695 lshpkrlem6 38587 athgt 38929 2llnjN 39040 dalaw 39359 lhpmcvr4N 39499 cdlemb2 39514 4atexlemex6 39547 cdlemd7 39677 cdleme01N 39694 cdleme02N 39695 cdleme0ex1N 39696 cdleme0ex2N 39697 cdleme7aa 39715 cdleme7c 39718 cdleme7d 39719 cdleme7e 39720 cdleme7ga 39721 cdleme7 39722 cdleme11a 39733 cdleme20k 39792 cdleme27cl 39839 cdleme42e 39952 cdleme42h 39955 cdleme42i 39956 cdlemf 40036 cdlemg2kq 40075 cdlemg2m 40077 cdlemg8a 40100 cdlemg11aq 40111 cdlemg10c 40112 cdlemg11b 40115 cdlemg17a 40134 cdlemg31b0N 40167 cdlemg31c 40172 cdlemg33c0 40175 cdlemg41 40191 cdlemh2 40289 cdlemn9 40678 dihglbcpreN 40773 dihmeetlem3N 40778 dihmeetlem13N 40792 pellex 42255 |
Copyright terms: Public domain | W3C validator |