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

Theorem simpr31 1264
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 1195 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2antr3 1191 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  oppccatid  17665  subccatid  17796  fuccatid  17922  setccatid  18034  catccatid  18056  estrccatid  18083  xpccatid  18140  nllyidm  22993  utoptop  23739  cgr3tr4  35024  seglecgr12im  35082  paddasslem9  38699  cdlemd1  39069  cdlemf2  39433  cdlemk34  39781  dihmeetlem18N  40195  dihmeetlem19N  40196  isthincd2  47658  mndtccatid  47713
  Copyright terms: Public domain W3C validator