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  4351  funprg  5305  fsnunf  5759  f1oiso2  5871  tfrlemibxssdm  6382  ecopovtrn  6688  ecopovtrng  6691  dftap2  7313  addassnqg  7444  ltsonq  7460  ltanqg  7462  ltmnqg  7463  addassnq0  7524  recexprlem1ssl  7695  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1lem  7842  mulextsr1  7843  axmulass  7935  axdistr  7936  dmdcanap  8743  lediv2  8912  ltdiv23  8913  lediv23  8914  xaddass2  9939  xlt2add  9949  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  expdivap  10664  leisorel  10911  bdtrilem  11385  xrbdtri  11422  fldivndvdslt  12079  prmexpb  12292  pcpremul  12434  pcdiv  12443  pcqmul  12444  pcqdiv  12448  4sqlem12  12543  f1ocpbllem  12896  ercpbl  12917  erlecpbl  12918  cmn4  13378  ablsub4  13386  abladdsub4  13387  cnptoprest  14418  ssblps  14604  ssbl  14605  tgqioo  14734  plyadd  14930  plymul  14931  rplogbchbase  15123