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  4829  omopth2  6818  ltmul1a  9848  xaddass  10817  xlemul2a  10857  dvdsadd2b  12880  pockthg  13262  efgred  15368  ptbasin  17597  basqtop  17731  xrsmopn  18831  br4  25370  axpasch  25828  axcontlem4  25854  btwnintr  25901  btwnexch3  25902  btwnouttr2  25904  cgrxfr  25937  lineext  25958  btwnconn1lem13  25981  btwnconn1lem14  25982  btwnconn3  25985  brsegle  25990  brsegle2  25991  segleantisym  25997  outsideofeu  26013  lineunray  26029  lineelsb2  26030  qirropth  26908  mzpcong  26974  jm2.26  27010  aomclem6  27071  psgnunilem4  27335  cvrcmp  29920  atcvrj2b  30068  3dimlem3  30097  3dimlem3OLDN  30098  3dim3  30105  ps-1  30113  lplnnle2at  30177  2llnm3N  30205  lvolnle3at  30218  4atlem0a  30229  4atlem3  30232  4atlem3a  30233  lnatexN  30415  paddasslem8  30463  paddasslem9  30464  paddasslem10  30465  paddasslem12  30467  paddasslem13  30468  lhp2lt  30637  lhpexle2lem  30645  lhpexle3  30648  lhpmcvr3  30661  lhpat3  30682  4atex  30712  ltrnideq  30811  ltrnatlw  30819  trlnle  30822  trlval4  30824  cdlemd4  30837  cdlemd5  30838  cdleme16  30921  cdleme21  30973  cdleme21k  30974  cdleme27cl  31002  cdleme27N  31005  cdleme29ex  31010  cdleme43fsv1snlem  31056  cdleme40m  31103  cdleme46f2g2  31129  cdleme46f2g1  31130  trlord  31205  cdlemg8  31267  cdlemg15a  31291  cdlemg16z  31295  cdlemg18a  31314  cdlemg24  31324  cdlemg38  31351  cdlemg40  31353  trlcone  31364  cdlemj2  31458  tendoid0  31461  tendoconid  31465  cdlemk34  31546  cdlemk38  31551  cdlemkid4  31570  cdlemk35s-id  31574  cdlemk39s-id  31576  cdlemk53  31593  tendospcanN  31660  cdlemm10N  31755  dihvalcqpre  31872  dihopelvalcpre  31885  dihord5b  31896  dihglblem5apreN  31928  dihmeetlem16N  31959  dihmeetlem17N  31960  dvh3dim3N  32086
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