Theorem simp2r 1027

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

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

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 983

This theorem is referenced by:  simpl2r  1054  simpr2r  1060  simp12r  1114  simp22r  1120  simp32r  1126  issod  4384  funprg  5343  fsnunf  5807  f1oiso2  5919  tfrlemibxssdm  6436  ecopovtrn  6742  ecopovtrng  6745  dftap2  7398  addassnqg  7530  ltsonq  7546  ltanqg  7548  ltmnqg  7549  addassnq0  7610  recexprlem1ssl  7781  mulasssrg  7906  distrsrg  7907  lttrsr  7910  ltsosr  7912  ltasrg  7918  mulextsr1lem  7928  mulextsr1  7929  axmulass  8021  axdistr  8022  dmdcanap  8830  lediv2  8999  ltdiv23  9000  lediv23  9001  xaddass2  10027  xlt2add  10037  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  expdivap  10772  leisorel  11019  swrdspsleq  11158  pfxeq  11187  ccatopth2  11208  bdtrilem  11665  xrbdtri  11702  fldivndvdslt  12363  prmexpb  12588  pcpremul  12731  pcdiv  12740  pcqmul  12741  pcqdiv  12745  4sqlem12  12840  f1ocpbllem  13257  ercpbl  13278  erlecpbl  13279  cmn4  13756  ablsub4  13764  abladdsub4  13765  cnptoprest  14826  ssblps  15012  ssbl  15013  tgqioo  15142  plyadd  15338  plymul  15339  rplogbchbase  15537