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  4365  funprg  5323  fsnunf  5783  f1oiso2  5895  tfrlemibxssdm  6412  ecopovtrn  6718  ecopovtrng  6721  dftap2  7362  addassnqg  7494  ltsonq  7510  ltanqg  7512  ltmnqg  7513  addassnq0  7574  recexprlem1ssl  7745  mulasssrg  7870  distrsrg  7871  lttrsr  7874  ltsosr  7876  ltasrg  7882  mulextsr1lem  7892  mulextsr1  7893  axmulass  7985  axdistr  7986  dmdcanap  8794  lediv2  8963  ltdiv23  8964  lediv23  8965  xaddass2  9991  xlt2add  10001  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  expdivap  10733  leisorel  10980  bdtrilem  11521  xrbdtri  11558  fldivndvdslt  12219  prmexpb  12444  pcpremul  12587  pcdiv  12596  pcqmul  12597  pcqdiv  12601  4sqlem12  12696  f1ocpbllem  13113  ercpbl  13134  erlecpbl  13135  cmn4  13612  ablsub4  13620  abladdsub4  13621  cnptoprest  14682  ssblps  14868  ssbl  14869  tgqioo  14998  plyadd  15194  plymul  15195  rplogbchbase  15393