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

Theorem simpr33 1364
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 1253 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜒)
213ad2antr3 1242 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  oppccatid  16693  subccatid  16820  fuccatid  16943  setccatid  17048  catccatid  17066  estrccatid  17086  xpccatid  17143  nllyidm  21621  utoptop  22366  cgr3tr4  32672  paddasslem9  35849  cdlemd1  36219  cdlemf2  36583  cdlemk34  36931  dihmeetlem18N  37345  dihmeetlem19N  37346
  Copyright terms: Public domain W3C validator