Theorem simp3r 1052

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

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

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 1006

This theorem is referenced by:  simpl3r  1079  simpr3r  1085  simp13r  1139  simp23r  1145  simp33r  1151  issod  4416  tfisi  4685  fvun1  5712  f1oiso2  5967  tfrlem5  6479  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  ecopovtrn  6800  ecopovtrng  6803  dftap2  7469  addassnqg  7601  ltsonq  7617  ltanqg  7619  ltmnqg  7620  addassnq0  7681  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1lem  7999  mulextsr1  8000  axmulass  8092  axdistr  8093  reapmul1  8774  mulcanap  8844  mulcanap2  8845  divassap  8869  divdirap  8876  div11ap  8879  apmul1  8967  ltdiv1  9047  ltmuldiv  9053  ledivmul  9056  lemuldiv  9060  lediv2  9070  ltdiv23  9071  lediv23  9072  xaddass2  10104  xlt2add  10114  modqdi  10653  expaddzap  10844  expmulzap  10846  leisorel  11100  resqrtcl  11589  xrbdtri  11836  dvdsgcd  12582  rpexp12i  12726  pythagtriplem4  12840  pythagtriplem11  12846  pythagtriplem13  12848  pcpremul  12865  pceu  12867  pcqmul  12875  pcqdiv  12879  f1ocpbllem  13392  ercpbl  13413  erlecpbl  13414  cmn4  13891  ablsub4  13899  abladdsub4  13900  lidlsubcl  14500  psmetlecl  15057  xmetlecl  15090  xblcntrps  15136  xblcntr  15137