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

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

Proof of Theorem simpl33
StepHypRef Expression
1 simpl3 1185 . 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:  ax5seglem3a  26643  ax5seg  26651  numclwwlk1lem2foa  28060  br8d  30289  br8  32889  nosupres  33104  cgrextend  33366  segconeq  33368  trisegint  33386  ifscgr  33402  cgrsub  33403  btwnxfr  33414  seglecgr12im  33468  segletr  33472  atbtwn  36462  4atlem10b  36621  4atlem11  36625  4atlem12  36628  2lplnj  36636  paddasslem4  36839  paddasslem7  36842  pmodlem1  36862  4atex2  37093  trlval3  37203  arglem1N  37206  cdleme0moN  37241  cdleme20  37340  cdleme21j  37352  cdleme28c  37388  cdleme38n  37480  cdlemg6c  37636  cdlemg6  37639  cdlemg7N  37642  cdlemg16  37673  cdlemg16ALTN  37674  cdlemg16zz  37676  cdlemg20  37701  cdlemg22  37703  cdlemg37  37705  cdlemg31d  37716  cdlemg29  37721  cdlemg33b  37723  cdlemg33  37727  cdlemg46  37751  cdlemk25-3  37920
  Copyright terms: Public domain W3C validator