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

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

Proof of Theorem simpr1l
StepHypRef Expression
1 simp1l 1083 . 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  16295  subccatid  16422  setccatid  16650  catccatid  16668  estrccatid  16688  xpccatid  16744  gsmsymgreqlem1  17766  dmdprdsplit  18362  neiptopnei  20841  neitr  20889  neitx  21315  tx1stc  21358  utop3cls  21960  metustsym  22265  ax5seg  25713  3pthdlem1  26884  frgrwopreg  27038  esumpcvgval  29913  esum2d  29928  ifscgr  31785  brofs2  31818  brifs2  31819  btwnconn1lem8  31835  btwnconn1lem12  31839  seglecgr12im  31851  unbdqndv2  32136  lhp2lt  34753  cdlemd1  34951  cdleme3b  34982  cdleme3c  34983  cdleme3e  34985  cdlemf2  35316  cdlemg4c  35366  cdlemn11pre  35965  dihmeetlem12N  36073  stoweidlem60  39571
  Copyright terms: Public domain W3C validator