MPE Home 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