Theorem simp3r 1029

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

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

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 983

This theorem is referenced by:  simpl3r  1056  simpr3r  1062  simp13r  1116  simp23r  1122  simp33r  1128  issod  4384  tfisi  4653  fvun1  5668  f1oiso2  5919  tfrlem5  6423  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  ecopovtrn  6742  ecopovtrng  6745  dftap2  7398  addassnqg  7530  ltsonq  7546  ltanqg  7548  ltmnqg  7549  addassnq0  7610  mulasssrg  7906  distrsrg  7907  lttrsr  7910  ltsosr  7912  ltasrg  7918  mulextsr1lem  7928  mulextsr1  7929  axmulass  8021  axdistr  8022  reapmul1  8703  mulcanap  8773  mulcanap2  8774  divassap  8798  divdirap  8805  div11ap  8808  apmul1  8896  ltdiv1  8976  ltmuldiv  8982  ledivmul  8985  lemuldiv  8989  lediv2  8999  ltdiv23  9000  lediv23  9001  xaddass2  10027  xlt2add  10037  modqdi  10574  expaddzap  10765  expmulzap  10767  leisorel  11019  resqrtcl  11455  xrbdtri  11702  dvdsgcd  12448  rpexp12i  12592  pythagtriplem4  12706  pythagtriplem11  12712  pythagtriplem13  12714  pcpremul  12731  pceu  12733  pcqmul  12741  pcqdiv  12745  f1ocpbllem  13257  ercpbl  13278  erlecpbl  13279  cmn4  13756  ablsub4  13764  abladdsub4  13765  lidlsubcl  14364  psmetlecl  14921  xmetlecl  14954  xblcntrps  15000  xblcntr  15001