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

Theorem simpr31 1260
 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 1191 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2antr3 1187 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  oppccatid  17060  subccatid  17188  fuccatid  17311  setccatid  17423  catccatid  17441  estrccatid  17461  xpccatid  17517  nllyidm  22202  utoptop  22948  cgr3tr4  33937  seglecgr12im  33995  paddasslem9  37438  cdlemd1  37808  cdlemf2  38172  cdlemk34  38520  dihmeetlem18N  38934  dihmeetlem19N  38935
 Copyright terms: Public domain W3C validator