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

Theorem simpl33 1253
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 1190 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl3 1184 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ax5seglem3a  26728  ax5seg  26736  numclwwlk1lem2foa  28143  br8d  30378  br8  33106  nosupres  33321  cgrextend  33583  segconeq  33585  trisegint  33603  ifscgr  33619  cgrsub  33620  btwnxfr  33631  seglecgr12im  33685  segletr  33689  atbtwn  36741  4atlem10b  36900  4atlem11  36904  4atlem12  36907  2lplnj  36915  paddasslem4  37118  paddasslem7  37121  pmodlem1  37141  4atex2  37372  trlval3  37482  arglem1N  37485  cdleme0moN  37520  cdleme20  37619  cdleme21j  37631  cdleme28c  37667  cdleme38n  37759  cdlemg6c  37915  cdlemg6  37918  cdlemg7N  37921  cdlemg16  37952  cdlemg16ALTN  37953  cdlemg16zz  37955  cdlemg20  37980  cdlemg22  37982  cdlemg37  37984  cdlemg31d  37995  cdlemg29  38000  cdlemg33b  38002  cdlemg33  38006  cdlemg46  38030  cdlemk25-3  38199
  Copyright terms: Public domain W3C validator