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

Theorem simpl32 1252
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 1189 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl3 1184 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  initoeu2lem2  18037  mulmarep1gsum2  22567  tsmsxp  24150  noinfres  27752  ax5seg  28872  br8d  32530  br8  35578  cgrextend  35832  segconeq  35834  trisegint  35852  ifscgr  35868  cgrsub  35869  btwnxfr  35880  seglecgr12im  35934  segletr  35938  exatleN  39103  atbtwn  39145  3dim1  39166  3dim2  39167  2llnjaN  39265  4atlem10b  39304  4atlem11  39308  4atlem12  39311  2lplnj  39319  cdlemb  39493  paddasslem4  39522  pmodlem1  39545  4atex2  39776  trlval3  39886  arglem1N  39889  cdleme0moN  39924  cdleme17b  39986  cdleme20  40023  cdleme21j  40035  cdleme28c  40071  cdleme35h2  40156  cdleme38n  40163  cdlemg6c  40319  cdlemg6  40322  cdlemg7N  40325  cdlemg11a  40336  cdlemg12e  40346  cdlemg16  40356  cdlemg16ALTN  40357  cdlemg16zz  40359  cdlemg20  40384  cdlemg22  40386  cdlemg37  40388  cdlemg31d  40399  cdlemg29  40404  cdlemg33b  40406  cdlemg33  40410  cdlemg39  40415  cdlemg42  40428  cdlemk25-3  40603
  Copyright terms: Public domain W3C validator