Theorem simp2r 1026

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

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

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 982

This theorem is referenced by:  simpl2r  1053  simpr2r  1059  simp12r  1113  simp22r  1119  simp32r  1125  issod  4355  funprg  5309  fsnunf  5765  f1oiso2  5877  tfrlemibxssdm  6394  ecopovtrn  6700  ecopovtrng  6703  dftap2  7334  addassnqg  7466  ltsonq  7482  ltanqg  7484  ltmnqg  7485  addassnq0  7546  recexprlem1ssl  7717  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1lem  7864  mulextsr1  7865  axmulass  7957  axdistr  7958  dmdcanap  8766  lediv2  8935  ltdiv23  8936  lediv23  8937  xaddass2  9962  xlt2add  9972  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  expdivap  10699  leisorel  10946  bdtrilem  11421  xrbdtri  11458  fldivndvdslt  12119  prmexpb  12344  pcpremul  12487  pcdiv  12496  pcqmul  12497  pcqdiv  12501  4sqlem12  12596  f1ocpbllem  13012  ercpbl  13033  erlecpbl  13034  cmn4  13511  ablsub4  13519  abladdsub4  13520  cnptoprest  14559  ssblps  14745  ssbl  14746  tgqioo  14875  plyadd  15071  plymul  15072  rplogbchbase  15270