Theorem simp2l 1054

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 1050	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2l  1081  simpr2l  1087  simp12l  1141  simp22l  1147  simp32l  1153  issod  4464  funprg  5431  fsnunf  5915  f1oiso2  6033  ecopovtrn  6906  ecopovtrng  6909  dftap2  7618  addassnqg  7750  ltsonq  7766  ltanqg  7768  ltmnqg  7769  addassnq0  7830  recexprlem1ssu  8002  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1lem  8148  mulextsr1  8149  axmulass  8241  axdistr  8242  dmdcanap  9055  ltdiv2  9220  lediv2  9224  ltdiv23  9225  lediv23  9226  xaddass  10282  xaddass2  10283  xlt2add  10293  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  expdivap  11042  leisorel  11305  swrdspsleq  11455  pfxeq  11484  ccatopth2  11505  bdtrilem  12024  bdtri  12025  xrbdtri  12061  fsumsplitsnun  12205  prmexpb  12949  pcpremul  13095  pcdiv  13104  pcqmul  13105  pcqdiv  13109  4sqlem12  13204  f1ocpbllem  13684  ercpbl  13705  erlecpbl  13706  cmn4  14192  ablsub4  14201  abladdsub4  14202  rng1zrlem  14342  cnptoprest  15431  ssblps  15617  ssbl  15618  tgqioo  15747  plyadd  15943  plymul  15944  rplogbchbase  16147  dichmul0or  16926