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

Theorem simpl3l 1012
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 985 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantr 452 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  tfisi  4830  omopth2  6819  ltmul1a  9851  xaddass  10820  xlemul2a  10860  dvdsadd2b  12884  pockthg  13266  efgred  15372  ptbasin  17601  basqtop  17735  xrsmopn  18835  br4  25373  axpasch  25872  axcontlem4  25898  btwnintr  25945  btwnexch3  25946  btwnouttr2  25948  cgrxfr  25981  lineext  26002  btwnconn1lem13  26025  btwnconn1lem14  26026  btwnconn3  26029  brsegle  26034  brsegle2  26035  segleantisym  26041  outsideofeu  26057  lineunray  26073  lineelsb2  26074  qirropth  26962  mzpcong  27028  jm2.26  27064  aomclem6  27125  psgnunilem4  27388  cvrcmp  30018  atcvrj2b  30166  3dimlem3  30195  3dimlem3OLDN  30196  3dim3  30203  ps-1  30211  lplnnle2at  30275  2llnm3N  30303  lvolnle3at  30316  4atlem0a  30327  4atlem3  30330  4atlem3a  30331  lnatexN  30513  paddasslem8  30561  paddasslem9  30562  paddasslem10  30563  paddasslem12  30565  paddasslem13  30566  lhp2lt  30735  lhpexle2lem  30743  lhpexle3  30746  lhpmcvr3  30759  lhpat3  30780  4atex  30810  ltrnideq  30909  ltrnatlw  30917  trlnle  30920  trlval4  30922  cdlemd4  30935  cdlemd5  30936  cdleme16  31019  cdleme21  31071  cdleme21k  31072  cdleme27cl  31100  cdleme27N  31103  cdleme29ex  31108  cdleme43fsv1snlem  31154  cdleme40m  31201  cdleme46f2g2  31227  cdleme46f2g1  31228  trlord  31303  cdlemg8  31365  cdlemg15a  31389  cdlemg16z  31393  cdlemg18a  31412  cdlemg24  31422  cdlemg38  31449  cdlemg40  31451  trlcone  31462  cdlemj2  31556  tendoid0  31559  tendoconid  31563  cdlemk34  31644  cdlemk38  31649  cdlemkid4  31668  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk53  31691  tendospcanN  31758  cdlemm10N  31853  dihvalcqpre  31970  dihopelvalcpre  31983  dihord5b  31994  dihglblem5apreN  32026  dihmeetlem16N  32057  dihmeetlem17N  32058  dvh3dim3N  32184
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator