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  4414  tfisi  4683  fvun1  5708  f1oiso2  5963  tfrlem5  6475  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  ecopovtrn  6796  ecopovtrng  6799  dftap2  7460  addassnqg  7592  ltsonq  7608  ltanqg  7610  ltmnqg  7611  addassnq0  7672  mulasssrg  7968  distrsrg  7969  lttrsr  7972  ltsosr  7974  ltasrg  7980  mulextsr1lem  7990  mulextsr1  7991  axmulass  8083  axdistr  8084  reapmul1  8765  mulcanap  8835  mulcanap2  8836  divassap  8860  divdirap  8867  div11ap  8870  apmul1  8958  ltdiv1  9038  ltmuldiv  9044  ledivmul  9047  lemuldiv  9051  lediv2  9061  ltdiv23  9062  lediv23  9063  xaddass2  10095  xlt2add  10105  modqdi  10644  expaddzap  10835  expmulzap  10837  leisorel  11091  resqrtcl  11580  xrbdtri  11827  dvdsgcd  12573  rpexp12i  12717  pythagtriplem4  12831  pythagtriplem11  12837  pythagtriplem13  12839  pcpremul  12856  pceu  12858  pcqmul  12866  pcqdiv  12870  f1ocpbllem  13383  ercpbl  13404  erlecpbl  13405  cmn4  13882  ablsub4  13890  abladdsub4  13891  lidlsubcl  14491  psmetlecl  15048  xmetlecl  15081  xblcntrps  15127  xblcntr  15128