Theorem simpll2 1063

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1027	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

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

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  fidceq  7055  fidifsnen  7056  en2eqpr  7098  iunfidisj  7144  ctssdc  7311  cauappcvgprlemlol  7866  caucvgprlemlol  7889  caucvgprprlemlol  7917  elfzonelfzo  10474  qbtwnre  10515  nn0ltexp2  10970  hashun  11067  swrdclg  11230  xrmaxltsup  11818  subcn2  11871  prodmodclem2  12137  divalglemex  12482  divalglemeuneg  12483  dvdslegcd  12534  lcmledvds  12641  modprmn0modprm0  12828  qexpz  12924  rnglidlmcl  14493  iscnp4  14941  cnrest2  14959  blssps  15150  blss  15151  bdbl  15226  metcnp3  15234  addcncntoplem  15284  cdivcncfap  15327  lgsfcl2  15734  lgsdir  15763  lgsne0  15766  subupgr  16123  clwwlknonex2  16289