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

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

Proof of Theorem simpl32
StepHypRef Expression
1 simpl2 1184 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl3 1179 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  initoeu2lem2  17263  mulmarep1gsum2  21111  tsmsxp  22690  ax5seg  26651  br8d  30289  br8  32889  cgrextend  33366  segconeq  33368  trisegint  33386  ifscgr  33402  cgrsub  33403  btwnxfr  33414  seglecgr12im  33468  segletr  33472  exatleN  36420  atbtwn  36462  3dim1  36483  3dim2  36484  2llnjaN  36582  4atlem10b  36621  4atlem11  36625  4atlem12  36628  2lplnj  36636  cdlemb  36810  paddasslem4  36839  pmodlem1  36862  4atex2  37093  trlval3  37203  arglem1N  37206  cdleme0moN  37241  cdleme17b  37303  cdleme20  37340  cdleme21j  37352  cdleme28c  37388  cdleme35h2  37473  cdleme38n  37480  cdlemg6c  37636  cdlemg6  37639  cdlemg7N  37642  cdlemg11a  37653  cdlemg12e  37663  cdlemg16  37673  cdlemg16ALTN  37674  cdlemg16zz  37676  cdlemg20  37701  cdlemg22  37703  cdlemg37  37705  cdlemg31d  37716  cdlemg29  37721  cdlemg33b  37723  cdlemg33  37727  cdlemg39  37732  cdlemg42  37745  cdlemk25-3  37920
  Copyright terms: Public domain W3C validator