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  16886  mulmarep1gsum2  20602  tsmsxp  22179  ax5seg  26038  elwwlks2ons3OLD  27097  br8d  29750  br8  31974  cgrextend  32442  segconeq  32444  trisegint  32462  ifscgr  32478  cgrsub  32479  btwnxfr  32490  seglecgr12im  32544  segletr  32548  exatleN  35211  atbtwn  35253  3dim1  35274  3dim2  35275  2llnjaN  35373  4atlem10b  35412  4atlem11  35416  4atlem12  35419  2lplnj  35427  cdlemb  35601  paddasslem4  35630  pmodlem1  35653  4atex2  35884  trlval3  35995  arglem1N  35998  cdleme0moN  36033  cdleme17b  36095  cdleme20  36132  cdleme21j  36144  cdleme28c  36180  cdleme35h2  36265  cdleme38n  36272  cdlemg6c  36428  cdlemg6  36431  cdlemg7N  36434  cdlemg11a  36445  cdlemg12e  36455  cdlemg16  36465  cdlemg16ALTN  36466  cdlemg16zz  36468  cdlemg20  36493  cdlemg22  36495  cdlemg37  36497  cdlemg31d  36508  cdlemg29  36513  cdlemg33b  36515  cdlemg33  36519  cdlemg39  36524  cdlemg42  36537  cdlemk25-3  36712
  Copyright terms: Public domain W3C validator