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

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

Proof of Theorem simpr31
StepHypRef Expression
1 simp31 1090 . 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  fuccatid  16452  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  nllyidm  21102  utoptop  21848  cgr3tr4  31329  seglecgr12im  31387  paddasslem9  34132  cdlemd1  34503  cdlemf2  34868  cdlemk34  35216  dihmeetlem18N  35631  dihmeetlem19N  35632
 Copyright terms: Public domain W3C validator