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

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

Proof of Theorem simpr33
StepHypRef Expression
1 simpr3 1193 . 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  16967  subccatid  17094  fuccatid  17217  setccatid  17322  catccatid  17340  estrccatid  17360  xpccatid  17416  nllyidm  22072  utoptop  22818  cgr3tr4  33520  paddasslem9  37002  cdlemd1  37372  cdlemf2  37736  cdlemk34  38084  dihmeetlem18N  38498  dihmeetlem19N  38499
  Copyright terms: Public domain W3C validator