Theorem simp3r 1028

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

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

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 982

This theorem is referenced by:  simpl3r  1055  simpr3r  1061  simp13r  1115  simp23r  1121  simp33r  1127  issod  4355  tfisi  4624  fvun1  5630  f1oiso2  5877  tfrlem5  6376  tfr1onlembxssdm  6405  tfrcllembxssdm  6418  ecopovtrn  6695  ecopovtrng  6698  dftap2  7323  addassnqg  7454  ltsonq  7470  ltanqg  7472  ltmnqg  7473  addassnq0  7534  mulasssrg  7830  distrsrg  7831  lttrsr  7834  ltsosr  7836  ltasrg  7842  mulextsr1lem  7852  mulextsr1  7853  axmulass  7945  axdistr  7946  reapmul1  8627  mulcanap  8697  mulcanap2  8698  divassap  8722  divdirap  8729  div11ap  8732  apmul1  8820  ltdiv1  8900  ltmuldiv  8906  ledivmul  8909  lemuldiv  8913  lediv2  8923  ltdiv23  8924  lediv23  8925  xaddass2  9950  xlt2add  9960  modqdi  10489  expaddzap  10680  expmulzap  10682  leisorel  10934  resqrtcl  11199  xrbdtri  11446  dvdsgcd  12192  rpexp12i  12336  pythagtriplem4  12450  pythagtriplem11  12456  pythagtriplem13  12458  pcpremul  12475  pceu  12477  pcqmul  12485  pcqdiv  12489  f1ocpbllem  13000  ercpbl  13021  erlecpbl  13022  cmn4  13482  ablsub4  13490  abladdsub4  13491  lidlsubcl  14090  psmetlecl  14617  xmetlecl  14650  xblcntrps  14696  xblcntr  14697