Theorem simp3r 1050

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

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

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 1004

This theorem is referenced by:  simpl3r  1077  simpr3r  1083  simp13r  1137  simp23r  1143  simp33r  1149  issod  4410  tfisi  4679  fvun1  5700  f1oiso2  5951  tfrlem5  6460  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  ecopovtrn  6779  ecopovtrng  6782  dftap2  7437  addassnqg  7569  ltsonq  7585  ltanqg  7587  ltmnqg  7588  addassnq0  7649  mulasssrg  7945  distrsrg  7946  lttrsr  7949  ltsosr  7951  ltasrg  7957  mulextsr1lem  7967  mulextsr1  7968  axmulass  8060  axdistr  8061  reapmul1  8742  mulcanap  8812  mulcanap2  8813  divassap  8837  divdirap  8844  div11ap  8847  apmul1  8935  ltdiv1  9015  ltmuldiv  9021  ledivmul  9024  lemuldiv  9028  lediv2  9038  ltdiv23  9039  lediv23  9040  xaddass2  10066  xlt2add  10076  modqdi  10614  expaddzap  10805  expmulzap  10807  leisorel  11059  resqrtcl  11540  xrbdtri  11787  dvdsgcd  12533  rpexp12i  12677  pythagtriplem4  12791  pythagtriplem11  12797  pythagtriplem13  12799  pcpremul  12816  pceu  12818  pcqmul  12826  pcqdiv  12830  f1ocpbllem  13343  ercpbl  13364  erlecpbl  13365  cmn4  13842  ablsub4  13850  abladdsub4  13851  lidlsubcl  14451  psmetlecl  15008  xmetlecl  15041  xblcntrps  15087  xblcntr  15088