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

Theorem simpr32 1264
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpr32 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜓)

Proof of Theorem simpr32
StepHypRef Expression
1 simpr2 1195 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜓)
213ad2antr3 1190 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  oppccatid  17661  subccatid  17792  fuccatid  17918  setccatid  18030  catccatid  18052  estrccatid  18079  xpccatid  18136  nllyidm  22984  utoptop  23730  omndmul2  32217  cgr3tr4  35012  paddasslem9  38687  cdlemd1  39057  cdlemf2  39421  cdlemk34  39769  dihmeetlem18N  40183  isthincd2  47611  mndtccatid  47666
  Copyright terms: Public domain W3C validator