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

Theorem simpl3l 1043
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 1016 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantr 465 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  tfisi  6490  omopth2  7044  ltmul1a  10199  xaddass  11233  xlemul2a  11273  dvdsadd2b  13596  pockthg  13988  psgnunilem4  16024  efgred  16266  ptbasin  19172  basqtop  19306  xrsmopn  20411  axpasch  23209  axcontlem4  23235  br4  27590  btwnintr  28072  btwnexch3  28073  btwnouttr2  28075  cgrxfr  28108  lineext  28129  btwnconn1lem13  28152  btwnconn1lem14  28153  btwnconn3  28156  brsegle  28161  brsegle2  28162  segleantisym  28168  outsideofeu  28184  lineunray  28200  lineelsb2  28201  qirropth  29275  mzpcong  29341  jm2.26  29377  aomclem6  29438  cvrcmp  33024  atcvrj2b  33172  3dimlem3  33201  3dimlem3OLDN  33202  3dim3  33209  ps-1  33217  lplnnle2at  33281  2llnm3N  33309  lvolnle3at  33322  4atlem0a  33333  4atlem3  33336  4atlem3a  33337  lnatexN  33519  paddasslem8  33567  paddasslem9  33568  paddasslem10  33569  paddasslem12  33571  paddasslem13  33572  lhp2lt  33741  lhpexle2lem  33749  lhpexle3  33752  lhpmcvr3  33765  lhpat3  33786  4atex  33816  trlval2  33903  ltrnideq  33915  ltrnatlw  33923  trlnle  33926  trlval4  33928  cdlemd4  33941  cdlemd5  33942  cdleme16  34025  cdleme21  34077  cdleme21k  34078  cdleme27cl  34106  cdleme27N  34109  cdleme29ex  34114  cdleme43fsv1snlem  34160  cdleme40m  34207  cdleme46f2g2  34233  cdleme46f2g1  34234  trlord  34309  cdlemg8  34371  cdlemg15a  34395  cdlemg16z  34399  cdlemg18a  34418  cdlemg24  34428  cdlemg38  34455  cdlemg40  34457  trlcone  34468  cdlemj2  34562  tendoid0  34565  tendoconid  34569  cdlemk34  34650  cdlemk38  34655  cdlemkid4  34674  cdlemk35s-id  34678  cdlemk39s-id  34680  cdlemk53  34697  tendospcanN  34764  cdlemm10N  34859  dihvalcqpre  34976  dihopelvalcpre  34989  dihord5b  35000  dihglblem5apreN  35032  dihmeetlem16N  35063  dihmeetlem17N  35064  dvh3dim3N  35190
  Copyright terms: Public domain W3C validator