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

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

Proof of Theorem simpr1l
StepHypRef Expression
1 simp1l 1078 . 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  dmdprdsplit  18269  neiptopnei  20746  neitr  20794  neitx  21220  tx1stc  21263  utop3cls  21865  metustsym  22170  ax5seg  25618  frgrawopreg  26576  esumpcvgval  29467  esum2d  29482  ifscgr  31321  brofs2  31354  brifs2  31355  btwnconn1lem8  31371  btwnconn1lem12  31375  seglecgr12im  31387  unbdqndv2  31672  lhp2lt  34305  cdlemd1  34503  cdleme3b  34534  cdleme3c  34535  cdleme3e  34537  cdlemf2  34868  cdlemg4c  34918  cdlemn11pre  35517  dihmeetlem12N  35625  stoweidlem60  38953  3pthdlem1  41331  frgrwopreg  41486
 Copyright terms: Public domain W3C validator