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

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

Proof of Theorem simpr31
StepHypRef Expression
1 simp31 1095 . 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  16319  subccatid  16446  fuccatid  16569  setccatid  16674  catccatid  16692  estrccatid  16712  xpccatid  16768  nllyidm  21232  utoptop  21978  cgr3tr4  31854  seglecgr12im  31912  paddasslem9  34633  cdlemd1  35004  cdlemf2  35369  cdlemk34  35717  dihmeetlem18N  36132  dihmeetlem19N  36133
  Copyright terms: Public domain W3C validator