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

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

Proof of Theorem simpr33
StepHypRef Expression
1 simp33 1097 . 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  cgr3tr4  31793  paddasslem9  34580  cdlemd1  34951  cdlemf2  35316  cdlemk34  35664  dihmeetlem18N  36079  dihmeetlem19N  36080
 Copyright terms: Public domain W3C validator