![]() |
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 770 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr1 1189 | 1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: poxp2 8076 poxp3 8083 oppccatid 17606 subccatid 17737 setccatid 17975 catccatid 17997 estrccatid 18024 xpccatid 18081 gsmsymgreqlem1 19217 dmdprdsplit 19831 neiptopnei 22499 neitr 22547 neitx 22974 tx1stc 23017 utop3cls 23619 metustsym 23927 ax5seg 27929 clwwlkccat 28976 3pthdlem1 29150 esumpcvgval 32734 esum2d 32749 ifscgr 34675 brofs2 34708 brifs2 34709 btwnconn1lem8 34725 btwnconn1lem12 34729 seglecgr12im 34741 unbdqndv2 35020 lhp2lt 38510 cdlemd1 38707 cdleme3b 38738 cdleme3c 38739 cdleme3e 38741 cdlemf2 39071 cdlemg4c 39121 cdlemn11pre 39719 dihmeetlem12N 39827 stoweidlem60 44387 isthincd2 47144 mndtccatid 47199 |
Copyright terms: Public domain | W3C validator |