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

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

Proof of Theorem simpr2l
StepHypRef Expression
1 simp2l 1080 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
21adantl 481 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  oppccatid  16202  subccatid  16329  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  gsmsymgreqlem1  17673  kerf1hrm  18566  nllyidm  21102  ax5seg  25618  segconeq  31287  ifscgr  31321  brofs2  31354  brifs2  31355  idinside  31361  btwnconn1lem8  31371  btwnconn1lem12  31375  segcon2  31382  segletr  31391  outsidele  31409  unbdqndv2  31672  lplnexllnN  33868  paddasslem9  34132  pmodlem2  34151  lhp2lt  34305  cdlemc3  34498  cdlemc4  34499  cdlemd1  34503  cdleme3b  34534  cdleme3c  34535  cdleme42ke  34791  cdlemg4c  34918  3pthdlem1  41331
 Copyright terms: Public domain W3C validator