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 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  oppccatid  17763  subccatid  17892  fuccatid  18018  setccatid  18130  catccatid  18152  estrccatid  18177  xpccatid  18234  nllyidm  23498  utoptop  24244  omndmul2  33090  cgr3tr4  36054  paddasslem9  39831  cdlemd1  40201  cdlemf2  40565  cdlemk34  40913  dihmeetlem18N  41327  isthincd2  49111  mndtccatid  49239
  Copyright terms: Public domain W3C validator