Theorem simp3r 973

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 109	. 2 |- ( ( ch /\ th ) -> th )
2	1	3ad2ant3 967	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 925

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  simpl3r  1000  simpr3r  1006  simp13r  1060  simp23r  1066  simp33r  1072  issod  4155  tfisi  4415  fvun1  5383  f1oiso2  5620  tfrlem5  6093  tfr1onlembxssdm  6122  tfrcllembxssdm  6135  ecopovtrn  6403  ecopovtrng  6406  addassnqg  7002  ltsonq  7018  ltanqg  7020  ltmnqg  7021  addassnq0  7082  mulasssrg  7365  distrsrg  7366  lttrsr  7369  ltsosr  7371  ltasrg  7377  mulextsr1lem  7386  mulextsr1  7387  axmulass  7469  axdistr  7470  reapmul1  8133  mulcanap  8195  mulcanap2  8196  divassap  8218  divdirap  8225  div11ap  8228  apmul1  8316  ltdiv1  8390  ltmuldiv  8396  ledivmul  8399  lemuldiv  8403  lediv2  8413  ltdiv23  8414  lediv23  8415  modqdi  9860  expaddzap  10060  expmulzap  10062  leisorel  10303  resqrtcl  10523  dvdsgcd  11340  rpexp12i  11473