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

Theorem simpl3l 1051
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 1024 . 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 973
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 975
This theorem is referenced by:  tfisi  6677  omopth2  7233  ltmul1a  10391  xaddass  11441  xlemul2a  11481  dvdsadd2b  13887  pockthg  14283  psgnunilem4  16328  efgred  16572  ptbasin  19841  basqtop  19975  xrsmopn  21080  axpasch  23948  axcontlem4  23974  br4  28792  btwnintr  29274  btwnexch3  29275  btwnouttr2  29277  cgrxfr  29310  lineext  29331  btwnconn1lem13  29354  btwnconn1lem14  29355  btwnconn3  29358  brsegle  29363  brsegle2  29364  segleantisym  29370  outsideofeu  29386  lineunray  29402  lineelsb2  29403  qirropth  30476  mzpcong  30542  jm2.26  30576  aomclem6  30637  limcleqr  31214  fourierdlem42  31477  cvrcmp  34098  atcvrj2b  34246  3dimlem3  34275  3dimlem3OLDN  34276  3dim3  34283  ps-1  34291  lplnnle2at  34355  2llnm3N  34383  lvolnle3at  34396  4atlem0a  34407  4atlem3  34410  4atlem3a  34411  lnatexN  34593  paddasslem8  34641  paddasslem9  34642  paddasslem10  34643  paddasslem12  34645  paddasslem13  34646  lhp2lt  34815  lhpexle2lem  34823  lhpexle3  34826  lhpmcvr3  34839  lhpat3  34860  4atex  34890  trlval2  34977  ltrnideq  34989  ltrnatlw  34997  trlnle  35000  trlval4  35002  cdlemd4  35015  cdlemd5  35016  cdleme16  35099  cdleme21  35151  cdleme21k  35152  cdleme27cl  35180  cdleme27N  35183  cdleme29ex  35188  cdleme43fsv1snlem  35234  cdleme40m  35281  cdleme46f2g2  35307  cdleme46f2g1  35308  trlord  35383  cdlemg8  35445  cdlemg15a  35469  cdlemg16z  35473  cdlemg18a  35492  cdlemg24  35502  cdlemg38  35529  cdlemg40  35531  trlcone  35542  cdlemj2  35636  tendoid0  35639  tendoconid  35643  cdlemk34  35724  cdlemk38  35729  cdlemkid4  35748  cdlemk35s-id  35752  cdlemk39s-id  35754  cdlemk53  35771  tendospcanN  35838  cdlemm10N  35933  dihvalcqpre  36050  dihopelvalcpre  36063  dihord5b  36074  dihglblem5apreN  36106  dihmeetlem16N  36137  dihmeetlem17N  36138  dvh3dim3N  36264
  Copyright terms: Public domain W3C validator