Theorem simp3r 1026

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3r	|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ch /\ th ) -> th )
2	1	3ad2ant3 1020	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )

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:  simpl3r  1053  simpr3r  1059  simp13r  1113  simp23r  1119  simp33r  1125  issod  4319  tfisi  4586  fvun1  5582  f1oiso2  5827  tfrlem5  6314  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  ecopovtrn  6631  ecopovtrng  6634  dftap2  7249  addassnqg  7380  ltsonq  7396  ltanqg  7398  ltmnqg  7399  addassnq0  7460  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  reapmul1  8551  mulcanap  8621  mulcanap2  8622  divassap  8646  divdirap  8653  div11ap  8656  apmul1  8744  ltdiv1  8824  ltmuldiv  8830  ledivmul  8833  lemuldiv  8837  lediv2  8847  ltdiv23  8848  lediv23  8849  xaddass2  9869  xlt2add  9879  modqdi  10391  expaddzap  10563  expmulzap  10565  leisorel  10816  resqrtcl  11037  xrbdtri  11283  dvdsgcd  12012  rpexp12i  12154  pythagtriplem4  12267  pythagtriplem11  12273  pythagtriplem13  12275  pcpremul  12292  pceu  12294  pcqmul  12302  pcqdiv  12306  f1ocpbllem  12730  ercpbl  12749  erlecpbl  12750  cmn4  13106  ablsub4  13114  abladdsub4  13115  psmetlecl  13770  xmetlecl  13803  xblcntrps  13849  xblcntr  13850