Theorem simpll2 1068

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 1032	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> 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

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

This theorem is used by:  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ctssdc  7453  cauappcvgprlemlol  8014  caucvgprlemlol  8037  caucvgprprlemlol  8065  elfzonelfzo  10648  qbtwnre  10691  nn0ltexp2  11147  hashun  11245  swrdclg  11422  xrmaxltsup  12024  subcn2  12077  prodmodclem2  12344  divalglemex  12689  divalglemeuneg  12690  dvdslegcd  12741  lcmledvds  12848  modprmn0modprm0  13035  qexpz  13131  rnglidlmcl  14817  iscnp4  15319  cnrest2  15337  blssps  15528  blss  15529  bdbl  15604  metcnp3  15612  addcncntoplem  15662  cdivcncfap  15705  lgsfcl2  16125  lgsdir  16154  lgsne0  16157  subupgr  16514  clwwlknonex2  16680