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

Theorem simpl3l 1060
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 1033 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
21adantr 466 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  tfisi  6699  omopth2  7293  ltmul1a  10453  xaddass  11535  xlemul2a  11575  swrdsbslen  12789  dvdsadd2b  14325  pockthg  14813  psgnunilem4  17089  efgred  17333  ptbasin  20523  basqtop  20657  xrsmopn  21741  axpasch  24817  axcontlem4  24843  br4  30185  btwnintr  30571  btwnexch3  30572  btwnouttr2  30574  cgrxfr  30607  lineext  30628  btwnconn1lem13  30651  btwnconn1lem14  30652  btwnconn3  30655  brsegle  30660  brsegle2  30661  segleantisym  30667  outsideofeu  30683  lineunray  30699  lineelsb2  30700  cvrcmp  32558  atcvrj2b  32706  3dimlem3  32735  3dimlem3OLDN  32736  3dim3  32743  ps-1  32751  lplnnle2at  32815  2llnm3N  32843  lvolnle3at  32856  4atlem0a  32867  4atlem3  32870  4atlem3a  32871  lnatexN  33053  paddasslem8  33101  paddasslem9  33102  paddasslem10  33103  paddasslem12  33105  paddasslem13  33106  lhp2lt  33275  lhpexle2lem  33283  lhpexle3  33286  lhpmcvr3  33299  lhpat3  33320  4atex  33350  trlval2  33438  ltrnideq  33450  ltrnatlw  33458  trlnle  33461  trlval4  33463  cdlemd4  33476  cdlemd5  33477  cdleme16  33560  cdleme21  33613  cdleme21k  33614  cdleme27cl  33642  cdleme27N  33645  cdleme29ex  33650  cdleme43fsv1snlem  33696  cdleme40m  33743  cdleme46f2g2  33769  cdleme46f2g1  33770  trlord  33845  cdlemg8  33907  cdlemg15a  33931  cdlemg16z  33935  cdlemg18a  33954  cdlemg24  33964  cdlemg38  33991  cdlemg40  33993  trlcone  34004  cdlemj2  34098  tendoid0  34101  tendoconid  34105  cdlemk34  34186  cdlemk38  34191  cdlemkid4  34210  cdlemk35s-id  34214  cdlemk39s-id  34216  cdlemk53  34233  tendospcanN  34300  cdlemm10N  34395  dihvalcqpre  34512  dihopelvalcpre  34525  dihord5b  34536  dihglblem5apreN  34568  dihmeetlem16N  34599  dihmeetlem17N  34600  dvh3dim3N  34726  qirropth  35462  mzpcong  35528  jm2.26  35563  aomclem6  35623  limcleqr  37297  fourierdlem42  37580
  Copyright terms: Public domain W3C validator