Theorem simp3r 1021

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

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

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 975

This theorem is referenced by:  simpl3r  1048  simpr3r  1054  simp13r  1108  simp23r  1114  simp33r  1120  issod  4304  tfisi  4571  fvun1  5562  f1oiso2  5806  tfrlem5  6293  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  ltsonq  7360  ltanqg  7362  ltmnqg  7363  addassnq0  7424  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  reapmul1  8514  mulcanap  8583  mulcanap2  8584  divassap  8607  divdirap  8614  div11ap  8617  apmul1  8705  ltdiv1  8784  ltmuldiv  8790  ledivmul  8793  lemuldiv  8797  lediv2  8807  ltdiv23  8808  lediv23  8809  xaddass2  9827  xlt2add  9837  modqdi  10348  expaddzap  10520  expmulzap  10522  leisorel  10772  resqrtcl  10993  xrbdtri  11239  dvdsgcd  11967  rpexp12i  12109  pythagtriplem4  12222  pythagtriplem11  12228  pythagtriplem13  12230  pcpremul  12247  pceu  12249  pcqmul  12257  pcqdiv  12261  psmetlecl  13128  xmetlecl  13161  xblcntrps  13207  xblcntr  13208