Theorem simp3r 1053

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

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

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 1007

This theorem is referenced by:  simpl3r  1080  simpr3r  1086  simp13r  1140  simp23r  1146  simp33r  1152  issod  4422  tfisi  4691  fvun1  5721  f1oiso2  5978  tfrlem5  6523  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  ecopovtrn  6844  ecopovtrng  6847  dftap2  7530  addassnqg  7662  ltsonq  7678  ltanqg  7680  ltmnqg  7681  addassnq0  7742  mulasssrg  8038  distrsrg  8039  lttrsr  8042  ltsosr  8044  ltasrg  8050  mulextsr1lem  8060  mulextsr1  8061  axmulass  8153  axdistr  8154  reapmul1  8834  mulcanap  8904  mulcanap2  8905  divassap  8929  divdirap  8936  div11ap  8939  apmul1  9027  ltdiv1  9107  ltmuldiv  9113  ledivmul  9116  lemuldiv  9120  lediv2  9130  ltdiv23  9131  lediv23  9132  xaddass2  10166  xlt2add  10176  modqdi  10717  expaddzap  10908  expmulzap  10910  leisorel  11164  resqrtcl  11669  xrbdtri  11916  dvdsgcd  12663  rpexp12i  12807  pythagtriplem4  12921  pythagtriplem11  12927  pythagtriplem13  12929  pcpremul  12946  pceu  12948  pcqmul  12956  pcqdiv  12960  f1ocpbllem  13473  ercpbl  13494  erlecpbl  13495  cmn4  13972  ablsub4  13980  abladdsub4  13981  lidlsubcl  14583  psmetlecl  15145  xmetlecl  15178  xblcntrps  15224  xblcntr  15225