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

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

Proof of Theorem simpl31
StepHypRef Expression
1 simpl1 1188 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl3 1184 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ax5seglem3a  26702  ax5seg  26710  uhgrwkspth  27522  usgr2wlkspth  27526  br8d  30347  br8  32999  nosupres  33214  cgrextend  33476  segconeq  33478  trisegint  33496  ifscgr  33512  cgrsub  33513  btwnxfr  33524  seglecgr12im  33578  segletr  33582  atbtwn  36622  3dim1  36643  2llnjaN  36742  4atlem10b  36781  4atlem11  36785  4atlem12  36788  2lplnj  36796  paddasslem4  36999  pmodlem1  37022  4atex2  37253  trlval3  37363  arglem1N  37366  cdleme0moN  37401  cdleme17b  37463  cdleme20  37500  cdleme21j  37512  cdleme28c  37548  cdleme35h2  37633  cdlemg6c  37796  cdlemg6  37799  cdlemg7N  37802  cdlemg8c  37805  cdlemg11a  37813  cdlemg11b  37818  cdlemg12e  37823  cdlemg16  37833  cdlemg16ALTN  37834  cdlemg16zz  37836  cdlemg20  37861  cdlemg22  37863  cdlemg37  37865  cdlemg31d  37876  cdlemg33b  37883  cdlemg33  37887  cdlemg39  37892  cdlemg42  37905  cdlemk25-3  38080  cdlemk33N  38085  cdlemk53b  38132
  Copyright terms: Public domain W3C validator