MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl11 Unicode version

Theorem simpl11 1030
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl11  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ph )

Proof of Theorem simpl11
StepHypRef Expression
1 simp11 985 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pythagtriplem4  12888  tsmsxp  17853  br8  24184  brbtwn2  24605  ax5seg  24638  btwndiff  24722  ifscgr  24739  seglecgr12im  24805  lkrshp  29917  cvlcvr1  30151  atbtwn  30257  3dimlem3  30272  3dimlem3OLDN  30273  1cvratex  30284  llnmlplnN  30350  4atlem3  30407  4atlem3a  30408  4atlem11  30420  4atlem12  30423  lnatexN  30590  cdlemb  30605  paddasslem4  30634  paddasslem10  30640  pmodlem1  30657  llnexchb2lem  30679  llnexchb2  30680  arglem1N  31001  cdlemd4  31012  cdlemd9  31017  cdlemd  31018  cdleme16  31096  cdleme20  31135  cdleme21i  31146  cdleme21k  31149  cdleme27N  31180  cdleme28c  31183  cdlemefrs29bpre0  31207  cdlemefrs29clN  31210  cdlemefrs32fva  31211  cdleme41sn3a  31244  cdleme32fva  31248  cdleme40n  31279  cdlemg12e  31458  cdlemg15a  31466  cdlemg15  31467  cdlemg16ALTN  31469  cdlemg16z  31470  cdlemg20  31496  cdlemg22  31498  cdlemg29  31516  cdlemg38  31526  cdlemk33N  31720  cdlemk56  31782  dihord11b  32034  dihord2pre  32037  dihord4  32070
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator