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

Theorem simpr32 1258
 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 1189 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜓)
213ad2antr3 1184 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1081 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 208  df-an 397  df-3an 1083 This theorem is referenced by:  oppccatid  16984  subccatid  17111  fuccatid  17234  setccatid  17339  catccatid  17357  estrccatid  17377  xpccatid  17433  nllyidm  22032  utoptop  22777  omndmul2  30646  cgr3tr4  33416  paddasslem9  36850  cdlemd1  37220  cdlemf2  37584  cdlemk34  37932  dihmeetlem18N  38346
 Copyright terms: Public domain W3C validator