![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr2l | 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 |
---|---|
simpr2l | ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl 770 | . 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑) | |
2 | 1 | 3ad2antr2 1190 | 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 ttrcltr 9657 ttrclss 9661 dmttrcl 9662 ttrclselem2 9667 oppccatid 17606 subccatid 17737 setccatid 17975 catccatid 17997 estrccatid 18024 xpccatid 18081 gsmsymgreqlem1 19217 kerf1ghm 20184 nllyidm 22856 noinfbnd1lem5 27091 ax5seg 27929 3pthdlem1 29150 segconeq 34641 ifscgr 34675 brofs2 34708 brifs2 34709 idinside 34715 btwnconn1lem8 34725 btwnconn1lem12 34729 segcon2 34736 segletr 34745 outsidele 34763 unbdqndv2 35020 lplnexllnN 38073 paddasslem9 38337 pmodlem2 38356 lhp2lt 38510 cdlemc3 38702 cdlemc4 38703 cdlemd1 38707 cdleme3b 38738 cdleme3c 38739 cdleme42ke 38994 cdlemg4c 39121 isthincd2 47144 mndtccatid 47199 |
Copyright terms: Public domain | W3C validator |