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

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

Proof of Theorem simpl33
StepHypRef Expression
1 simp33 1097 . 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  elwwlks2ons3  26717  br8d  29265  br8  31354  nosires  31577  cgrextend  31757  segconeq  31759  trisegint  31777  ifscgr  31793  cgrsub  31794  btwnxfr  31805  seglecgr12im  31859  segletr  31863  atbtwn  34212  4atlem10b  34371  4atlem11  34375  4atlem12  34378  2lplnj  34386  paddasslem4  34589  paddasslem7  34592  pmodlem1  34612  4atex2  34843  trlval3  34954  arglem1N  34957  cdleme0moN  34992  cdleme20  35092  cdleme21j  35104  cdleme28c  35140  cdleme38n  35232  cdlemg6c  35388  cdlemg6  35391  cdlemg7N  35394  cdlemg16  35425  cdlemg16ALTN  35426  cdlemg16zz  35428  cdlemg20  35453  cdlemg22  35455  cdlemg37  35457  cdlemg31d  35468  cdlemg29  35473  cdlemg33b  35475  cdlemg33  35479  cdlemg46  35503  cdlemk25-3  35672
  Copyright terms: Public domain W3C validator