MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl3l 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  4779  omopth2  6764  ltmul1a  9792  xaddass  10761  xlemul2a  10801  dvdsadd2b  12820  pockthg  13202  efgred  15308  ptbasin  17531  basqtop  17665  xrsmopn  18715  br4  25140  axpasch  25595  axcontlem4  25621  btwnintr  25668  btwnexch3  25669  btwnouttr2  25671  cgrxfr  25704  lineext  25725  btwnconn1lem13  25748  btwnconn1lem14  25749  btwnconn3  25752  brsegle  25757  brsegle2  25758  segleantisym  25764  outsideofeu  25780  lineunray  25796  lineelsb2  25797  qirropth  26663  mzpcong  26729  jm2.26  26765  aomclem6  26826  psgnunilem4  27090  cvrcmp  29399  atcvrj2b  29547  3dimlem3  29576  3dimlem3OLDN  29577  3dim3  29584  ps-1  29592  lplnnle2at  29656  2llnm3N  29684  lvolnle3at  29697  4atlem0a  29708  4atlem3  29711  4atlem3a  29712  lnatexN  29894  paddasslem8  29942  paddasslem9  29943  paddasslem10  29944  paddasslem12  29946  paddasslem13  29947  lhp2lt  30116  lhpexle2lem  30124  lhpexle3  30127  lhpmcvr3  30140  lhpat3  30161  4atex  30191  ltrnideq  30290  ltrnatlw  30298  trlnle  30301  trlval4  30303  cdlemd4  30316  cdlemd5  30317  cdleme16  30400  cdleme21  30452  cdleme21k  30453  cdleme27cl  30481  cdleme27N  30484  cdleme29ex  30489  cdleme43fsv1snlem  30535  cdleme40m  30582  cdleme46f2g2  30608  cdleme46f2g1  30609  trlord  30684  cdlemg8  30746  cdlemg15a  30770  cdlemg16z  30774  cdlemg18a  30793  cdlemg24  30803  cdlemg38  30830  cdlemg40  30832  trlcone  30843  cdlemj2  30937  tendoid0  30940  tendoconid  30944  cdlemk34  31025  cdlemk38  31030  cdlemkid4  31049  cdlemk35s-id  31053  cdlemk39s-id  31055  cdlemk53  31072  tendospcanN  31139  cdlemm10N  31234  dihvalcqpre  31351  dihopelvalcpre  31364  dihord5b  31375  dihglblem5apreN  31407  dihmeetlem16N  31438  dihmeetlem17N  31439  dvh3dim3N  31565
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