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

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

Proof of Theorem simpl32
StepHypRef Expression
1 simp32 1096 . 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:  initoeu2lem2  16586  mulmarep1gsum2  20299  tsmsxp  21868  ax5seg  25718  elwwlks2ons3  26717  br8d  29262  br8  31351  cgrextend  31754  segconeq  31756  trisegint  31774  ifscgr  31790  cgrsub  31791  btwnxfr  31802  seglecgr12im  31856  segletr  31860  exatleN  34167  atbtwn  34209  3dim1  34230  3dim2  34231  2llnjaN  34329  4atlem10b  34368  4atlem11  34372  4atlem12  34375  2lplnj  34383  cdlemb  34557  paddasslem4  34586  pmodlem1  34609  4atex2  34840  trlval3  34951  arglem1N  34954  cdleme0moN  34989  cdleme17b  35051  cdleme20  35089  cdleme21j  35101  cdleme28c  35137  cdleme35h2  35222  cdleme38n  35229  cdlemg6c  35385  cdlemg6  35388  cdlemg7N  35391  cdlemg11a  35402  cdlemg12e  35412  cdlemg16  35422  cdlemg16ALTN  35423  cdlemg16zz  35425  cdlemg20  35450  cdlemg22  35452  cdlemg37  35454  cdlemg31d  35465  cdlemg29  35470  cdlemg33b  35472  cdlemg33  35476  cdlemg39  35481  cdlemg42  35494  cdlemk25-3  35669
  Copyright terms: Public domain W3C validator