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

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

Proof of Theorem simpl3l
StepHypRef Expression
1 simp3l 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantr 451 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  tfisi  4649  omopth2  6582  ltmul1a  9605  xaddass  10569  xlemul2a  10609  dvdsadd2b  12571  pockthg  12953  efgred  15057  ptbasin  17272  basqtop  17402  xrsmopn  18318  br4  24115  axpasch  24569  axcontlem4  24595  btwnintr  24642  btwnexch3  24643  btwnouttr2  24645  cgrxfr  24678  lineext  24699  btwnconn1lem13  24722  btwnconn1lem14  24723  btwnconn3  24726  brsegle  24731  brsegle2  24732  segleantisym  24738  outsideofeu  24754  lineunray  24770  lineelsb2  24771  iccss3  25134  prjmapcp2  25170  cmprltr  25410  mulmulvec  25687  distsava  25689  idmon  25817  isconcl5ab  26102  qirropth  26993  mzpcong  27059  jm2.26  27095  aomclem6  27156  psgnunilem4  27420  cvrcmp  29473  atcvrj2b  29621  3dimlem3  29650  3dimlem3OLDN  29651  3dim3  29658  ps-1  29666  lplnnle2at  29730  2llnm3N  29758  lvolnle3at  29771  4atlem0a  29782  4atlem3  29785  4atlem3a  29786  lnatexN  29968  paddasslem8  30016  paddasslem9  30017  paddasslem10  30018  paddasslem12  30020  paddasslem13  30021  lhp2lt  30190  lhpexle2lem  30198  lhpexle3  30201  lhpmcvr3  30214  lhpat3  30235  4atex  30265  ltrnideq  30364  ltrnatlw  30372  trlnle  30375  trlval4  30377  cdlemd4  30390  cdlemd5  30391  cdleme16  30474  cdleme21  30526  cdleme21k  30527  cdleme27cl  30555  cdleme27N  30558  cdleme29ex  30563  cdleme43fsv1snlem  30609  cdleme40m  30656  cdleme46f2g2  30682  cdleme46f2g1  30683  trlord  30758  cdlemg8  30820  cdlemg15a  30844  cdlemg16z  30848  cdlemg18a  30867  cdlemg24  30877  cdlemg38  30904  cdlemg40  30906  trlcone  30917  cdlemj2  31011  tendoid0  31014  tendoconid  31018  cdlemk34  31099  cdlemk38  31104  cdlemkid4  31123  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53  31146  tendospcanN  31213  cdlemm10N  31308  dihvalcqpre  31425  dihopelvalcpre  31438  dihord5b  31449  dihglblem5apreN  31481  dihmeetlem16N  31512  dihmeetlem17N  31513  dvh3dim3N  31639
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