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  4321  funprg  5268  fsnunf  5719  f1oiso2  5831  tfrlemibxssdm  6331  ecopovtrn  6635  ecopovtrng  6638  dftap2  7253  addassnqg  7384  ltsonq  7400  ltanqg  7402  ltmnqg  7403  addassnq0  7464  recexprlem1ssl  7635  mulasssrg  7760  distrsrg  7761  lttrsr  7764  ltsosr  7766  ltasrg  7772  mulextsr1lem  7782  mulextsr1  7783  axmulass  7875  axdistr  7876  dmdcanap  8682  lediv2  8851  ltdiv23  8852  lediv23  8853  xaddass2  9873  xlt2add  9883  expaddzaplem  10566  expaddzap  10567  expmulzap  10569  expdivap  10574  leisorel  10820  bdtrilem  11250  xrbdtri  11287  fldivndvdslt  11943  prmexpb  12154  pcpremul  12296  pcdiv  12305  pcqmul  12306  pcqdiv  12310  f1ocpbllem  12737  ercpbl  12756  erlecpbl  12757  cmn4  13114  ablsub4  13122  abladdsub4  13123  cnptoprest  13879  ssblps  14065  ssbl  14066  tgqioo  14187  rplogbchbase  14508