Theorem simp3r 1011

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

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

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 965

This theorem is referenced by:  simpl3r  1038  simpr3r  1044  simp13r  1098  simp23r  1104  simp33r  1110  issod  4249  tfisi  4509  fvun1  5495  f1oiso2  5736  tfrlem5  6219  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  ecopovtrn  6534  ecopovtrng  6537  addassnqg  7214  ltsonq  7230  ltanqg  7232  ltmnqg  7233  addassnq0  7294  mulasssrg  7590  distrsrg  7591  lttrsr  7594  ltsosr  7596  ltasrg  7602  mulextsr1lem  7612  mulextsr1  7613  axmulass  7705  axdistr  7706  reapmul1  8381  mulcanap  8450  mulcanap2  8451  divassap  8474  divdirap  8481  div11ap  8484  apmul1  8572  ltdiv1  8650  ltmuldiv  8656  ledivmul  8659  lemuldiv  8663  lediv2  8673  ltdiv23  8674  lediv23  8675  xaddass2  9683  xlt2add  9693  modqdi  10196  expaddzap  10368  expmulzap  10370  leisorel  10612  resqrtcl  10833  xrbdtri  11077  dvdsgcd  11736  rpexp12i  11869  psmetlecl  12542  xmetlecl  12575  xblcntrps  12621  xblcntr  12622