![]() |
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 771 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr1 1187 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: poxp2 8167 poxp3 8174 oppccatid 17766 subccatid 17897 setccatid 18138 catccatid 18160 estrccatid 18187 xpccatid 18244 gsmsymgreqlem1 19463 dmdprdsplit 20082 neiptopnei 23156 neitr 23204 neitx 23631 tx1stc 23674 utop3cls 24276 metustsym 24584 ax5seg 28968 clwwlkccat 30019 3pthdlem1 30193 esumpcvgval 34059 esum2d 34074 ifscgr 36026 brofs2 36059 brifs2 36060 btwnconn1lem8 36076 btwnconn1lem12 36080 seglecgr12im 36092 unbdqndv2 36494 lhp2lt 39984 cdlemd1 40181 cdleme3b 40212 cdleme3c 40213 cdleme3e 40215 cdlemf2 40545 cdlemg4c 40595 cdlemn11pre 41193 dihmeetlem12N 41301 stoweidlem60 46016 isthincd2 48838 mndtccatid 48896 |
Copyright terms: Public domain | W3C validator |