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

Theorem simpl32 1255
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 1192 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl3 1187 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  initoeu2lem2  17898  mulmarep1gsum2  21919  tsmsxp  23502  noinfres  27066  ax5seg  27785  br8d  31427  br8  34221  cgrextend  34582  segconeq  34584  trisegint  34602  ifscgr  34618  cgrsub  34619  btwnxfr  34630  seglecgr12im  34684  segletr  34688  exatleN  37856  atbtwn  37898  3dim1  37919  3dim2  37920  2llnjaN  38018  4atlem10b  38057  4atlem11  38061  4atlem12  38064  2lplnj  38072  cdlemb  38246  paddasslem4  38275  pmodlem1  38298  4atex2  38529  trlval3  38639  arglem1N  38642  cdleme0moN  38677  cdleme17b  38739  cdleme20  38776  cdleme21j  38788  cdleme28c  38824  cdleme35h2  38909  cdleme38n  38916  cdlemg6c  39072  cdlemg6  39075  cdlemg7N  39078  cdlemg11a  39089  cdlemg12e  39099  cdlemg16  39109  cdlemg16ALTN  39110  cdlemg16zz  39112  cdlemg20  39137  cdlemg22  39139  cdlemg37  39141  cdlemg31d  39152  cdlemg29  39157  cdlemg33b  39159  cdlemg33  39163  cdlemg39  39168  cdlemg42  39181  cdlemk25-3  39356
  Copyright terms: Public domain W3C validator