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

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

Proof of Theorem simpl23
StepHypRef Expression
1 simp23 1094 . 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:  mulgdirlem  17493  brbtwn2  25685  ax5seglem3a  25710  ax5seg  25718  axpasch  25721  axeuclid  25743  br8d  29265  br8  31354  cgrextend  31757  segconeq  31759  segconeu  31760  trisegint  31777  ifscgr  31793  cgrsub  31794  cgrxfr  31804  lineext  31825  seglecgr12im  31859  segletr  31863  lineunray  31896  lineelsb2  31897  cvrcmp  34050  cvlsupr2  34110  atcvrj2b  34198  atexchcvrN  34206  3atlem3  34251  3atlem5  34253  lplnnle2at  34307  lplnllnneN  34322  4atlem3  34362  4atlem10b  34371  4atlem12  34378  2llnma3r  34554  paddasslem4  34589  paddasslem7  34592  paddasslem8  34593  paddasslem12  34597  paddasslem13  34598  paddasslem15  34600  pmodlem1  34612  pmodlem2  34613  atmod1i1m  34624  llnexchb2lem  34634  4atex2  34843  ltrnatlw  34950  arglem1N  34957  cdlemd4  34968  cdlemd5  34969  cdleme16  35052  cdleme20  35092  cdleme21k  35106  cdleme27N  35137  cdleme28c  35140  cdleme43fsv1snlem  35188  cdleme38n  35232  cdleme40n  35236  cdleme41snaw  35244  cdlemg6c  35388  cdlemg8c  35397  cdlemg8  35399  cdlemg12e  35415  cdlemg16ALTN  35426  cdlemg16zz  35428  cdlemg18a  35446  cdlemg20  35453  cdlemg22  35455  cdlemg37  35457  cdlemg31d  35468  cdlemg33  35479  cdlemg38  35483  cdlemg44b  35500  cdlemk33N  35677  cdlemk34  35678  cdlemk38  35683  cdlemk35s-id  35706  cdlemk39s-id  35708  cdlemk53b  35724  cdlemk53  35725  cdlemk55  35729  cdlemk35u  35732  cdlemk55u  35734  cdleml3N  35746  cdlemn11pre  35979
  Copyright terms: Public domain W3C validator