Theorem simp1r 1053

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1r	|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

Proof of Theorem simp1r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	3ad2ant1 1049	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1r  1080  simpr1r  1086  simp11r  1140  simp21r  1146  simp31r  1152  vtoclgft  2873  en2lp  4701  funprg  5431  nnsucsssuc  6765  ecopovtrn  6906  ecopovtrng  6909  addassnqg  7749  distrnqg  7754  ltsonq  7765  ltanqg  7767  ltmnqg  7768  distrnq0  7826  addassnq0  7829  prarloclem5  7867  recexprlem1ssl  8000  recexprlem1ssu  8001  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  dmdcanap  9052  lt2msq1  9215  lediv2  9221  xaddass2  10272  xlt2add  10282  modqdi  10829  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  swrdspsleq  11439  pfxeq  11468  bdtrilem  12005  xrbdtri  12042  bitsfzo  12722  prmexpb  12929  4sqlem18  13187  mgmsscl  13681  subgabl  14136  rng1zrlem  14258  cnptoprest  15340  ssblps  15526  ssbl  15527  rplogbchbase  16052  rplogbreexp  16055  relogbcxpbap  16067  lgssq  16159  uhgr2edg  16447