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

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

Proof of Theorem simpr32
StepHypRef Expression
1 simpr2 1193 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜓)
213ad2antr3 1188 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085
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 395  df-3an 1087
This theorem is referenced by:  oppccatid  17669  subccatid  17800  fuccatid  17926  setccatid  18038  catccatid  18060  estrccatid  18087  xpccatid  18144  nllyidm  23213  utoptop  23959  omndmul2  32500  cgr3tr4  35328  paddasslem9  39002  cdlemd1  39372  cdlemf2  39736  cdlemk34  40084  dihmeetlem18N  40498  isthincd2  47745  mndtccatid  47800
  Copyright terms: Public domain W3C validator