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

Theorem simpl32 1329
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 1230 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl3 1203 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  initoeu2lem2  16887  mulmarep1gsum2  20603  tsmsxp  22180  ax5seg  26039  elwwlks2ons3OLD  27098  br8d  29751  br8  31975  cgrextend  32443  segconeq  32445  trisegint  32463  ifscgr  32479  cgrsub  32480  btwnxfr  32491  seglecgr12im  32545  segletr  32549  exatleN  35212  atbtwn  35254  3dim1  35275  3dim2  35276  2llnjaN  35374  4atlem10b  35413  4atlem11  35417  4atlem12  35420  2lplnj  35428  cdlemb  35602  paddasslem4  35631  pmodlem1  35654  4atex2  35885  trlval3  35996  arglem1N  35999  cdleme0moN  36034  cdleme17b  36096  cdleme20  36133  cdleme21j  36145  cdleme28c  36181  cdleme35h2  36266  cdleme38n  36273  cdlemg6c  36429  cdlemg6  36432  cdlemg7N  36435  cdlemg11a  36446  cdlemg12e  36456  cdlemg16  36466  cdlemg16ALTN  36467  cdlemg16zz  36469  cdlemg20  36494  cdlemg22  36496  cdlemg37  36498  cdlemg31d  36509  cdlemg29  36514  cdlemg33b  36516  cdlemg33  36520  cdlemg39  36525  cdlemg42  36538  cdlemk25-3  36713
  Copyright terms: Public domain W3C validator