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

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

Proof of Theorem simpr31
StepHypRef Expression
1 simpr1 1194 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2antr3 1190 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  oppccatid  17779  subccatid  17910  fuccatid  18039  setccatid  18151  catccatid  18173  estrccatid  18200  xpccatid  18257  nllyidm  23518  utoptop  24264  cgr3tr4  36016  seglecgr12im  36074  paddasslem9  39785  cdlemd1  40155  cdlemf2  40519  cdlemk34  40867  dihmeetlem18N  41281  dihmeetlem19N  41282  isthincd2  48705  mndtccatid  48760
  Copyright terms: Public domain W3C validator