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

Theorem simpl31 1140
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl31 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜑)

Proof of Theorem simpl31
StepHypRef Expression
1 simp31 1095 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜑)
21adantr 481 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  ax5seglem3a  25710  ax5seg  25718  uhgrwkspth  26520  usgr2wlkspth  26524  br8d  29262  br8  31351  nosires  31574  cgrextend  31754  segconeq  31756  trisegint  31774  ifscgr  31790  cgrsub  31791  btwnxfr  31802  seglecgr12im  31856  segletr  31860  atbtwn  34209  3dim1  34230  2llnjaN  34329  4atlem10b  34368  4atlem11  34372  4atlem12  34375  2lplnj  34383  paddasslem4  34586  pmodlem1  34609  4atex2  34840  trlval3  34951  arglem1N  34954  cdleme0moN  34989  cdleme17b  35051  cdleme20  35089  cdleme21j  35101  cdleme28c  35137  cdleme35h2  35222  cdlemg6c  35385  cdlemg6  35388  cdlemg7N  35391  cdlemg8c  35394  cdlemg11a  35402  cdlemg11b  35407  cdlemg12e  35412  cdlemg16  35422  cdlemg16ALTN  35423  cdlemg16zz  35425  cdlemg20  35450  cdlemg22  35452  cdlemg37  35454  cdlemg31d  35465  cdlemg33b  35472  cdlemg33  35476  cdlemg39  35481  cdlemg42  35494  cdlemk25-3  35669  cdlemk33N  35674  cdlemk53b  35721
  Copyright terms: Public domain W3C validator