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

Theorem simpl3l 1013
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 986 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantr 453 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  tfisi  4841  omopth2  6830  ltmul1a  9864  xaddass  10833  xlemul2a  10873  dvdsadd2b  12897  pockthg  13279  efgred  15385  ptbasin  17614  basqtop  17748  xrsmopn  18848  br4  25386  axpasch  25885  axcontlem4  25911  btwnintr  25958  btwnexch3  25959  btwnouttr2  25961  cgrxfr  25994  lineext  26015  btwnconn1lem13  26038  btwnconn1lem14  26039  btwnconn3  26042  brsegle  26047  brsegle2  26048  segleantisym  26054  outsideofeu  26070  lineunray  26086  lineelsb2  26087  qirropth  26985  mzpcong  27051  jm2.26  27087  aomclem6  27148  psgnunilem4  27411  cvrcmp  30155  atcvrj2b  30303  3dimlem3  30332  3dimlem3OLDN  30333  3dim3  30340  ps-1  30348  lplnnle2at  30412  2llnm3N  30440  lvolnle3at  30453  4atlem0a  30464  4atlem3  30467  4atlem3a  30468  lnatexN  30650  paddasslem8  30698  paddasslem9  30699  paddasslem10  30700  paddasslem12  30702  paddasslem13  30703  lhp2lt  30872  lhpexle2lem  30880  lhpexle3  30883  lhpmcvr3  30896  lhpat3  30917  4atex  30947  ltrnideq  31046  ltrnatlw  31054  trlnle  31057  trlval4  31059  cdlemd4  31072  cdlemd5  31073  cdleme16  31156  cdleme21  31208  cdleme21k  31209  cdleme27cl  31237  cdleme27N  31240  cdleme29ex  31245  cdleme43fsv1snlem  31291  cdleme40m  31338  cdleme46f2g2  31364  cdleme46f2g1  31365  trlord  31440  cdlemg8  31502  cdlemg15a  31526  cdlemg16z  31530  cdlemg18a  31549  cdlemg24  31559  cdlemg38  31586  cdlemg40  31588  trlcone  31599  cdlemj2  31693  tendoid0  31696  tendoconid  31700  cdlemk34  31781  cdlemk38  31786  cdlemkid4  31805  cdlemk35s-id  31809  cdlemk39s-id  31811  cdlemk53  31828  tendospcanN  31895  cdlemm10N  31990  dihvalcqpre  32107  dihopelvalcpre  32120  dihord5b  32131  dihglblem5apreN  32163  dihmeetlem16N  32194  dihmeetlem17N  32195  dvh3dim3N  32321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator