Theorem simp2r 1055

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2r  1082  simpr2r  1088  simp12r  1142  simp22r  1148  simp32r  1154  issod  4464  funprg  5431  fsnunf  5915  f1oiso2  6033  tfrlemibxssdm  6598  ecopovtrn  6906  ecopovtrng  6909  dftap2  7617  addassnqg  7749  ltsonq  7765  ltanqg  7767  ltmnqg  7768  addassnq0  7829  recexprlem1ssl  8000  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  dmdcanap  9054  lediv2  9223  ltdiv23  9224  lediv23  9225  xaddass2  10282  xlt2add  10292  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  expdivap  11040  leisorel  11303  swrdspsleq  11453  pfxeq  11482  ccatopth2  11503  bdtrilem  12021  xrbdtri  12058  fldivndvdslt  12720  prmexpb  12946  pcpremul  13092  pcdiv  13101  pcqmul  13102  pcqdiv  13106  4sqlem12  13201  f1ocpbllem  13680  ercpbl  13701  erlecpbl  13702  cmn4  14157  ablsub4  14166  abladdsub4  14167  cnptoprest  15389  ssblps  15575  ssbl  15576  tgqioo  15705  plyadd  15901  plymul  15902  rplogbchbase  16105  dichmul0or  16858