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

Theorem simpl32 1246
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 1183 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl3 1178 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1078
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 1080
This theorem is referenced by:  initoeu2lem2  17092  mulmarep1gsum2  20855  tsmsxp  22434  ax5seg  26395  br8d  30026  br8  32545  cgrextend  33023  segconeq  33025  trisegint  33043  ifscgr  33059  cgrsub  33060  btwnxfr  33071  seglecgr12im  33125  segletr  33129  exatleN  36021  atbtwn  36063  3dim1  36084  3dim2  36085  2llnjaN  36183  4atlem10b  36222  4atlem11  36226  4atlem12  36229  2lplnj  36237  cdlemb  36411  paddasslem4  36440  pmodlem1  36463  4atex2  36694  trlval3  36804  arglem1N  36807  cdleme0moN  36842  cdleme17b  36904  cdleme20  36941  cdleme21j  36953  cdleme28c  36989  cdleme35h2  37074  cdleme38n  37081  cdlemg6c  37237  cdlemg6  37240  cdlemg7N  37243  cdlemg11a  37254  cdlemg12e  37264  cdlemg16  37274  cdlemg16ALTN  37275  cdlemg16zz  37277  cdlemg20  37302  cdlemg22  37304  cdlemg37  37306  cdlemg31d  37317  cdlemg29  37322  cdlemg33b  37324  cdlemg33  37328  cdlemg39  37333  cdlemg42  37346  cdlemk25-3  37521
  Copyright terms: Public domain W3C validator