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

Theorem simpl33 1338
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 1239 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl3 1231 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  ax5seglem3a  26020  ax5seg  26028  elwwlks2ons3OLD  27092  numclwwlk1lem2foa  27529  br8d  29743  br8  31963  nosupres  32169  cgrextend  32431  segconeq  32433  trisegint  32451  ifscgr  32467  cgrsub  32468  btwnxfr  32479  seglecgr12im  32533  segletr  32537  atbtwn  35221  4atlem10b  35380  4atlem11  35384  4atlem12  35387  2lplnj  35395  paddasslem4  35598  paddasslem7  35601  pmodlem1  35621  4atex2  35852  trlval3  35962  arglem1N  35965  cdleme0moN  36000  cdleme20  36099  cdleme21j  36111  cdleme28c  36147  cdleme38n  36239  cdlemg6c  36395  cdlemg6  36398  cdlemg7N  36401  cdlemg16  36432  cdlemg16ALTN  36433  cdlemg16zz  36435  cdlemg20  36460  cdlemg22  36462  cdlemg37  36464  cdlemg31d  36475  cdlemg29  36480  cdlemg33b  36482  cdlemg33  36486  cdlemg46  36510  cdlemk25-3  36679
  Copyright terms: Public domain W3C validator