![]() |
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 769 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr1 1188 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 397 df-3an 1089 |
This theorem is referenced by: poxp2 8128 poxp3 8135 oppccatid 17664 subccatid 17795 setccatid 18033 catccatid 18055 estrccatid 18082 xpccatid 18139 gsmsymgreqlem1 19297 dmdprdsplit 19916 neiptopnei 22635 neitr 22683 neitx 23110 tx1stc 23153 utop3cls 23755 metustsym 24063 ax5seg 28193 clwwlkccat 29240 3pthdlem1 29414 esumpcvgval 33071 esum2d 33086 ifscgr 35011 brofs2 35044 brifs2 35045 btwnconn1lem8 35061 btwnconn1lem12 35065 seglecgr12im 35077 unbdqndv2 35382 lhp2lt 38867 cdlemd1 39064 cdleme3b 39095 cdleme3c 39096 cdleme3e 39098 cdlemf2 39428 cdlemg4c 39478 cdlemn11pre 40076 dihmeetlem12N 40184 stoweidlem60 44766 isthincd2 47648 mndtccatid 47703 |
Copyright terms: Public domain | W3C validator |