Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp3ll | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp3ll | ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll 786 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant3 1077 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: f1oiso2 6502 omeu 7552 ntrivcvgmul 14473 tsmsxp 21768 tgqioo 22411 ovolunlem2 23073 plyadd 23777 plymul 23778 coeeu 23785 tghilberti2 25333 btwnconn1lem2 31365 btwnconn1lem3 31366 btwnconn1lem12 31375 athgt 33760 2llnjN 33871 4atlem12b 33915 lncmp 34087 cdlema2N 34096 cdlemc2 34497 cdleme5 34545 cdleme11a 34565 cdleme21ct 34635 cdleme21 34643 cdleme22eALTN 34651 cdleme24 34658 cdleme27cl 34672 cdleme27a 34673 cdleme28 34679 cdleme36a 34766 cdleme42b 34784 cdleme48fvg 34806 cdlemf 34869 cdlemk39 35222 cdlemkid1 35228 dihlsscpre 35541 dihord4 35565 dihord5apre 35569 dihmeetlem20N 35633 mapdh9a 36097 pellex 36417 jm2.27 36593 |
Copyright terms: Public domain | W3C validator |