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

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

Proof of Theorem simpr32
StepHypRef Expression
1 simp32 1091 . 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  omndmul2  29043  cgr3tr4  31329  paddasslem9  34132  cdlemd1  34503  cdlemf2  34868  cdlemk34  35216  dihmeetlem18N  35631
 Copyright terms: Public domain W3C validator