Theorem simp3r 1026

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

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

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 980

This theorem is referenced by:  simpl3r  1053  simpr3r  1059  simp13r  1113  simp23r  1119  simp33r  1125  issod  4320  tfisi  4587  fvun1  5583  f1oiso2  5828  tfrlem5  6315  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  ecopovtrn  6632  ecopovtrng  6635  dftap2  7250  addassnqg  7381  ltsonq  7397  ltanqg  7399  ltmnqg  7400  addassnq0  7461  mulasssrg  7757  distrsrg  7758  lttrsr  7761  ltsosr  7763  ltasrg  7769  mulextsr1lem  7779  mulextsr1  7780  axmulass  7872  axdistr  7873  reapmul1  8552  mulcanap  8622  mulcanap2  8623  divassap  8647  divdirap  8654  div11ap  8657  apmul1  8745  ltdiv1  8825  ltmuldiv  8831  ledivmul  8834  lemuldiv  8838  lediv2  8848  ltdiv23  8849  lediv23  8850  xaddass2  9870  xlt2add  9880  modqdi  10392  expaddzap  10564  expmulzap  10566  leisorel  10817  resqrtcl  11038  xrbdtri  11284  dvdsgcd  12013  rpexp12i  12155  pythagtriplem4  12268  pythagtriplem11  12274  pythagtriplem13  12276  pcpremul  12293  pceu  12295  pcqmul  12303  pcqdiv  12307  f1ocpbllem  12731  ercpbl  12750  erlecpbl  12751  cmn4  13108  ablsub4  13116  abladdsub4  13117  psmetlecl  13837  xmetlecl  13870  xblcntrps  13916  xblcntr  13917