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  4665  omopth2  6598  ltmul1a  9621  xaddass  10585  xlemul2a  10625  dvdsadd2b  12587  pockthg  12969  efgred  15073  ptbasin  17288  basqtop  17418  xrsmopn  18334  br4  24186  axpasch  24641  axcontlem4  24667  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  cgrxfr  24750  lineext  24771  btwnconn1lem13  24794  btwnconn1lem14  24795  btwnconn3  24798  brsegle  24803  brsegle2  24804  segleantisym  24810  outsideofeu  24826  lineunray  24842  lineelsb2  24843  iccss3  25237  prjmapcp2  25273  cmprltr  25513  mulmulvec  25790  distsava  25792  idmon  25920  isconcl5ab  26205  qirropth  27096  mzpcong  27162  jm2.26  27198  aomclem6  27259  psgnunilem4  27523  cvrcmp  30095  atcvrj2b  30243  3dimlem3  30272  3dimlem3OLDN  30273  3dim3  30280  ps-1  30288  lplnnle2at  30352  2llnm3N  30380  lvolnle3at  30393  4atlem0a  30404  4atlem3  30407  4atlem3a  30408  lnatexN  30590  paddasslem8  30638  paddasslem9  30639  paddasslem10  30640  paddasslem12  30642  paddasslem13  30643  lhp2lt  30812  lhpexle2lem  30820  lhpexle3  30823  lhpmcvr3  30836  lhpat3  30857  4atex  30887  ltrnideq  30986  ltrnatlw  30994  trlnle  30997  trlval4  30999  cdlemd4  31012  cdlemd5  31013  cdleme16  31096  cdleme21  31148  cdleme21k  31149  cdleme27cl  31177  cdleme27N  31180  cdleme29ex  31185  cdleme43fsv1snlem  31231  cdleme40m  31278  cdleme46f2g2  31304  cdleme46f2g1  31305  trlord  31380  cdlemg8  31442  cdlemg15a  31466  cdlemg16z  31470  cdlemg18a  31489  cdlemg24  31499  cdlemg38  31526  cdlemg40  31528  trlcone  31539  cdlemj2  31633  tendoid0  31636  tendoconid  31640  cdlemk34  31721  cdlemk38  31726  cdlemkid4  31745  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk53  31768  tendospcanN  31835  cdlemm10N  31930  dihvalcqpre  32047  dihopelvalcpre  32060  dihord5b  32071  dihglblem5apreN  32103  dihmeetlem16N  32134  dihmeetlem17N  32135  dvh3dim3N  32261
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