![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr1l | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
Ref | Expression |
---|---|
simpr1l | ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl 768 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr1 1185 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 |
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 1086 |
This theorem is referenced by: poxp2 8124 poxp3 8131 oppccatid 17666 subccatid 17797 setccatid 18038 catccatid 18060 estrccatid 18087 xpccatid 18144 gsmsymgreqlem1 19342 dmdprdsplit 19961 neiptopnei 22960 neitr 23008 neitx 23435 tx1stc 23478 utop3cls 24080 metustsym 24388 ax5seg 28668 clwwlkccat 29715 3pthdlem1 29889 esumpcvgval 33568 esum2d 33583 ifscgr 35512 brofs2 35545 brifs2 35546 btwnconn1lem8 35562 btwnconn1lem12 35566 seglecgr12im 35578 unbdqndv2 35878 lhp2lt 39366 cdlemd1 39563 cdleme3b 39594 cdleme3c 39595 cdleme3e 39597 cdlemf2 39927 cdlemg4c 39977 cdlemn11pre 40575 dihmeetlem12N 40683 stoweidlem60 45286 isthincd2 47870 mndtccatid 47925 |
Copyright terms: Public domain | W3C validator |