Theorem simp2l 1023

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	3ad2ant2 1019	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simpl2l  1050  simpr2l  1056  simp12l  1110  simp22l  1116  simp32l  1122  issod  4321  funprg  5268  fsnunf  5719  f1oiso2  5831  ecopovtrn  6635  ecopovtrng  6638  dftap2  7253  addassnqg  7384  ltsonq  7400  ltanqg  7402  ltmnqg  7403  addassnq0  7464  recexprlem1ssu  7636  mulasssrg  7760  distrsrg  7761  lttrsr  7764  ltsosr  7766  ltasrg  7772  mulextsr1lem  7782  mulextsr1  7783  axmulass  7875  axdistr  7876  dmdcanap  8682  ltdiv2  8847  lediv2  8851  ltdiv23  8852  lediv23  8853  xaddass  9872  xaddass2  9873  xlt2add  9883  expaddzaplem  10566  expaddzap  10567  expmulzap  10569  expdivap  10574  leisorel  10820  bdtrilem  11250  bdtri  11251  xrbdtri  11287  fsumsplitsnun  11430  prmexpb  12154  pcpremul  12296  pcdiv  12305  pcqmul  12306  pcqdiv  12310  f1ocpbllem  12737  ercpbl  12756  erlecpbl  12757  cmn4  13114  ablsub4  13122  abladdsub4  13123  cnptoprest  13879  ssblps  14065  ssbl  14066  tgqioo  14187  rplogbchbase  14508