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

Theorem simpl33 1330
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpl33 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl33
StepHypRef Expression
1 simpl3 1231 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl3 1202 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ax5seglem3a  26031  ax5seg  26039  elwwlks2ons3OLD  27103  numclwwlk1lem2foa  27540  br8d  29760  br8  31984  nosupres  32190  cgrextend  32452  segconeq  32454  trisegint  32472  ifscgr  32488  cgrsub  32489  btwnxfr  32500  seglecgr12im  32554  segletr  32558  atbtwn  35254  4atlem10b  35413  4atlem11  35417  4atlem12  35420  2lplnj  35428  paddasslem4  35631  paddasslem7  35634  pmodlem1  35654  4atex2  35885  trlval3  35996  arglem1N  35999  cdleme0moN  36034  cdleme20  36133  cdleme21j  36145  cdleme28c  36181  cdleme38n  36273  cdlemg6c  36429  cdlemg6  36432  cdlemg7N  36435  cdlemg16  36466  cdlemg16ALTN  36467  cdlemg16zz  36469  cdlemg20  36494  cdlemg22  36496  cdlemg37  36498  cdlemg31d  36509  cdlemg29  36514  cdlemg33b  36516  cdlemg33  36520  cdlemg46  36544  cdlemk25-3  36713
  Copyright terms: Public domain W3C validator