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

Theorem simpr32 1263
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 1194 . 2 ((𝜂 ∧ (𝜑𝜓𝜒)) → 𝜓)
213ad2antr3 1189 1 ((𝜂 ∧ (𝜃𝜏 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  oppccatid  17766  subccatid  17897  fuccatid  18026  setccatid  18138  catccatid  18160  estrccatid  18187  xpccatid  18244  nllyidm  23513  utoptop  24259  omndmul2  33072  cgr3tr4  36034  paddasslem9  39811  cdlemd1  40181  cdlemf2  40545  cdlemk34  40893  dihmeetlem18N  41307  isthincd2  48838  mndtccatid  48896
  Copyright terms: Public domain W3C validator