Theorem simp2r 1055

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

Assertion

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

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	3ad2ant2 1050	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ch )

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

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 1011

This theorem is referenced by:  simpl2r  1082  simpr2r  1088  simp12r  1142  simp22r  1148  simp32r  1154  issod  4459  funprg  5426  fsnunf  5906  f1oiso2  6023  tfrlemibxssdm  6588  ecopovtrn  6896  ecopovtrng  6899  dftap2  7607  addassnqg  7739  ltsonq  7755  ltanqg  7757  ltmnqg  7758  addassnq0  7819  recexprlem1ssl  7990  mulasssrg  8115  distrsrg  8116  lttrsr  8119  ltsosr  8121  ltasrg  8127  mulextsr1lem  8137  mulextsr1  8138  axmulass  8230  axdistr  8231  dmdcanap  9042  lediv2  9211  ltdiv23  9212  lediv23  9213  xaddass2  10251  xlt2add  10261  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  expdivap  11005  leisorel  11267  swrdspsleq  11417  pfxeq  11446  ccatopth2  11467  bdtrilem  11983  xrbdtri  12020  fldivndvdslt  12682  prmexpb  12907  pcpremul  13050  pcdiv  13059  pcqmul  13060  pcqdiv  13064  4sqlem12  13159  f1ocpbllem  13608  ercpbl  13629  erlecpbl  13630  cmn4  14085  ablsub4  14094  abladdsub4  14095  cnptoprest  15263  ssblps  15449  ssbl  15450  tgqioo  15579  plyadd  15775  plymul  15776  rplogbchbase  15975  dichmul0or  16674