MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpr2l Structured version   Visualization version   GIF version

Theorem simpr2l 1118
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr2l ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr2l
StepHypRef Expression
1 simp2l 1085 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
21adantl 482 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  oppccatid  16360  subccatid  16487  setccatid  16715  catccatid  16733  estrccatid  16753  xpccatid  16809  gsmsymgreqlem1  17831  kerf1hrm  18724  nllyidm  21273  ax5seg  25799  3pthdlem1  27004  segconeq  32092  ifscgr  32126  brofs2  32159  brifs2  32160  idinside  32166  btwnconn1lem8  32176  btwnconn1lem12  32180  segcon2  32187  segletr  32196  outsidele  32214  unbdqndv2  32477  lplnexllnN  34669  paddasslem9  34933  pmodlem2  34952  lhp2lt  35106  cdlemc3  35299  cdlemc4  35300  cdlemd1  35304  cdleme3b  35335  cdleme3c  35336  cdleme42ke  35592  cdlemg4c  35719
  Copyright terms: Public domain W3C validator