Theorem simp2r 1024

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

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

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 980

This theorem is referenced by:  simpl2r  1051  simpr2r  1057  simp12r  1111  simp22r  1117  simp32r  1123  issod  4320  funprg  5267  fsnunf  5717  f1oiso2  5828  tfrlemibxssdm  6328  ecopovtrn  6632  ecopovtrng  6635  dftap2  7250  addassnqg  7381  ltsonq  7397  ltanqg  7399  ltmnqg  7400  addassnq0  7461  recexprlem1ssl  7632  mulasssrg  7757  distrsrg  7758  lttrsr  7761  ltsosr  7763  ltasrg  7769  mulextsr1lem  7779  mulextsr1  7780  axmulass  7872  axdistr  7873  dmdcanap  8679  lediv2  8848  ltdiv23  8849  lediv23  8850  xaddass2  9870  xlt2add  9880  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  expdivap  10571  leisorel  10817  bdtrilem  11247  xrbdtri  11284  fldivndvdslt  11940  prmexpb  12151  pcpremul  12293  pcdiv  12302  pcqmul  12303  pcqdiv  12307  f1ocpbllem  12731  ercpbl  12750  erlecpbl  12751  cmn4  13108  ablsub4  13116  abladdsub4  13117  cnptoprest  13742  ssblps  13928  ssbl  13929  tgqioo  14050  rplogbchbase  14371