Theorem simp3r 1016

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 109	. 2 |- ( ( ch /\ th ) -> th )
2	1	3ad2ant3 1010	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl3r  1043  simpr3r  1049  simp13r  1103  simp23r  1109  simp33r  1115  issod  4296  tfisi  4563  fvun1  5551  f1oiso2  5794  tfrlem5  6278  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  ecopovtrn  6594  ecopovtrng  6597  addassnqg  7319  ltsonq  7335  ltanqg  7337  ltmnqg  7338  addassnq0  7399  mulasssrg  7695  distrsrg  7696  lttrsr  7699  ltsosr  7701  ltasrg  7707  mulextsr1lem  7717  mulextsr1  7718  axmulass  7810  axdistr  7811  reapmul1  8489  mulcanap  8558  mulcanap2  8559  divassap  8582  divdirap  8589  div11ap  8592  apmul1  8680  ltdiv1  8759  ltmuldiv  8765  ledivmul  8768  lemuldiv  8772  lediv2  8782  ltdiv23  8783  lediv23  8784  xaddass2  9802  xlt2add  9812  modqdi  10323  expaddzap  10495  expmulzap  10497  leisorel  10746  resqrtcl  10967  xrbdtri  11213  dvdsgcd  11941  rpexp12i  12083  pythagtriplem4  12196  pythagtriplem11  12202  pythagtriplem13  12204  pcpremul  12221  pceu  12223  pcqmul  12231  pcqdiv  12235  psmetlecl  12934  xmetlecl  12967  xblcntrps  13013  xblcntr  13014