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

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

Proof of Theorem simpr32
StepHypRef Expression
1 simp32 1096 . 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  fuccatid  16545  setccatid  16650  catccatid  16668  estrccatid  16688  xpccatid  16744  nllyidm  21197  utoptop  21943  omndmul2  29489  cgr3tr4  31793  paddasslem9  34580  cdlemd1  34951  cdlemf2  35316  cdlemk34  35664  dihmeetlem18N  36079
  Copyright terms: Public domain W3C validator