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  4319  funprg  5266  fsnunf  5716  f1oiso2  5827  tfrlemibxssdm  6327  ecopovtrn  6631  ecopovtrng  6634  dftap2  7249  addassnqg  7380  ltsonq  7396  ltanqg  7398  ltmnqg  7399  addassnq0  7460  recexprlem1ssl  7631  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  dmdcanap  8678  lediv2  8847  ltdiv23  8848  lediv23  8849  xaddass2  9869  xlt2add  9879  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  expdivap  10570  leisorel  10816  bdtrilem  11246  xrbdtri  11283  fldivndvdslt  11939  prmexpb  12150  pcpremul  12292  pcdiv  12301  pcqmul  12302  pcqdiv  12306  f1ocpbllem  12730  ercpbl  12749  erlecpbl  12750  cmn4  13106  ablsub4  13114  abladdsub4  13115  cnptoprest  13709  ssblps  13895  ssbl  13896  tgqioo  14017  rplogbchbase  14338